mathlib3

6e4c1b31 - feat(order/well_founded, data/fin/tuple/*, ...): add `well_founded.induction_bot`, `tuple.bubble_sort_induction` (#16536)

feat(order/well_founded, data/fin/tuple/*, ...): add `well_founded.induction_bot`, `tuple.bubble_sort_induction` (#16536) The main purpose of this PR is to add the following induction principle fir tuples. ```lean lemma tuple.bubble_sort_induction {n : ℕ} {α : Type*} [linear_order α] {f : fin n → α} {P : (fin n → α) → Prop} (hf : P f) (h : ∀ (g : fin n → α) (i j : fin n), i < j → g j < g i → P g → P (g ∘ equiv.swap i j)) : P (f ∘ sort f) ``` This is in a new file `data/fin/tuple/bubble_sort_induction`. The additional API lemmas needed for it are mostly added to `data/fin/tuple/sort` (and some in `data/list/perm` and `data/list/sort`). One of these lemmas is the following induction principle for well-founded relations. ```lean lemma well_founded.induction_bot {α} {r : α → α → Prop} (hwf : well_founded r) {a bot : α} {C : α → Prop} (ha : C a) (ih : ∀ b, b ≠ bot → C b → ∃ c, r c b ∧ C c) : C bot ``` See the discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.22sort.22.20a.20function/near/299289703).