Commit 2022-10-12 13:05 6e4c1b31

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.

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.

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.