awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
simp_rw :
  Eq (α := Option (Fin n))
    (if h : ∃ (i : Fin n), decide (p i) = true then some (Fin.find (fun (x : Fin n) ↦ decide (p x) = true) h) else none)
    (if h : ∃ (i : Fin n), p i then some (Fin.find p h) else none)
⊢ Eq (α := Option (Fin n)) (find? fun (x : Fin n) ↦ decide (p x))
    (if h : ∃ (i : Fin n), p i then some (Fin.find p h) else none)

Tactic:
simp_rw [find?_eq_dite, decide_eq_true_eq]

Premises used: Fin.find?_eq_dite, decide_eq_true_eq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
simp_rw :
  Option.get (if h : ∃ (i : Fin n), p i = true then some (Fin.find (fun (x : Fin n) ↦ p x = true) h) else none) ⋯ =
    Fin.find (fun (x : Fin n) ↦ p x = true) ⋯
⊢ (find? p).get ⋯ = Fin.find (fun (x : Fin n) ↦ p x = true) ⋯

Tactic:
simp_rw [find?_eq_dite, Option.get_dite]

Premises used: Fin.find?_eq_dite, Option.get_dite
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
m n : ℕ
p q : Fin n → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
i j : Fin n
h : ∃ (i : Fin n), p i
⊢ decide (p (h.choose (p := p))) = true

Tactic:
simp only [h.choose_spec, decide_true]

Premises used: Exists.choose_spec, decide_true
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (i : Fin n), p i
simp_rw : Option.get (if h : ∃ (i : Fin n), p i then some (Fin.find p h) else none) ⋯ = Fin.find p h
⊢ Option.get (find? fun (x : Fin n) ↦ decide (p x)) ⋯ = Fin.find p h

Tactic:
simp_rw [find?_decide_eq_dite, Option.get_dite]

Premises used: Option.get_dite, Fin.find?_decide_eq_dite
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (i : Fin n), p i
⊢ Membership.mem (γ := Option (Fin n)) (find? fun (b : Fin n) ↦ decide (p b)) (Fin.find p h)

Tactic:
grind [find?_eq_dite]

Premises used: Fin.find?_eq_dite
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Bool
i : Fin n
⊢ i ∈ find? p ↔ p i = true ∧ ∀ (j : Fin n), j < i → ¬p j = true

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Bool
h : ∃ (i : Fin n), p i = true
simp_rw :
  (if h : ∃ (i : Fin n), p i = true then some (Fin.find (fun (x : Fin n) ↦ p x = true) h) else none) =
    some (Fin.find (fun (x : Fin n) ↦ p x = true) h)
simp_rw₁ :
  (if h_1 : True then some (Fin.find (fun (x : Fin n) ↦ p x = true) ⋯) else none) =
    some (Fin.find (fun (x : Fin n) ↦ p x = true) h)
⊢ find? p = some (Fin.find (fun (x : Fin n) ↦ p x = true) h)

Tactic:
simp_rw [find?_eq_dite, h, dite_true]

Premises used: Fin.find?_eq_dite, dite_true
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
p : Fin n → Bool
h : (find? p).isSome = true
simp_rw :
  (if h : ∃ (i : Fin n), p i = true then some (Fin.find (fun (x : Fin n) ↦ p x = true) h) else none) =
    some (Fin.find (fun (x : Fin n) ↦ p x = true) ⋯)
simp_rw₁ :
  (if h_1 : True then some (Fin.find (fun (x : Fin n) ↦ p x = true) ⋯) else none) =
    some (Fin.find (fun (x : Fin n) ↦ p x = true) ⋯)
⊢ find? p = some (Fin.find (fun (x : Fin n) ↦ p x = true) ⋯)

Tactic:
simp_rw [find?_eq_dite, exists_eq_true_of_isSome_find? h, dite_true]

Premises used: Fin.find?_eq_dite, Fin.exists_eq_true_of_isSome_find?, dite_true
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : (↑k : ℕ) < (↑j : ℕ)
⊢ j.contractNth op g k = g k.castSucc

Tactic:
if_pos h

Premises used: if_pos, Fin.contractNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : (↑k : ℕ) = (↑j : ℕ)
⊢ ¬(↑k : ℕ) < (↑j : ℕ)

Tactic:
have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : (↑k : ℕ) = (↑j : ℕ)
this : ¬(↑k : ℕ) < (↑j : ℕ)
rw :
  (if (↑k : ℕ) < (↑j : ℕ) then g k.castSucc
    else if (↑k : ℕ) = (↑j : ℕ) then op (g k.castSucc) (g k.succ) else g k.succ) =
    op (g k.castSucc) (g k.succ)
rw₁ : (if (↑k : ℕ) = (↑j : ℕ) then op (g k.castSucc) (g k.succ) else g k.succ) = op (g k.castSucc) (g k.succ)
rw₂ rw₃ : op (g k.castSucc) (g k.succ) = op (g k.castSucc) (g k.succ)
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)

Tactic:
rw [contractNth, if_neg this, if_pos h]

Premises used: if_pos, if_neg, Fin.contractNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : (↑j : ℕ) < (↑k : ℕ)
rw :
  (if (↑k : ℕ) < (↑j : ℕ) then g k.castSucc
    else if (↑k : ℕ) = (↑j : ℕ) then op (g k.castSucc) (g k.succ) else g k.succ) =
    g k.succ
rw₁ : (if (↑k : ℕ) = (↑j : ℕ) then op (g k.castSucc) (g k.succ) else g k.succ) = g k.succ
rw₂ rw₃ : g k.succ = g k.succ
⊢ j.contractNth op g k = g k.succ

Tactic:
rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]

Premises used: Ne.symm, not_lt_of_gt, ne_of_lt, if_neg, Fin.contractNth
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
inl : ∀ (h : (↑k : ℕ) < (↑j : ℕ)), j.contractNth op g k = g (j.succAbove k)
inr : ∀ (h : (↑k : ℕ) = (↑j : ℕ)), j.contractNth op g k = g (j.succAbove k)
inr₁ : ∀ (h : (↑j : ℕ) < (↑k : ℕ)), j.contractNth op g k = g (j.succAbove k)
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rcases lt_trichotomy (k : ℕ) j with (h | h | h)

Premises used: Fin.val, lt_trichotomy
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
h : (↑k : ℕ) < (↑j : ℕ)
inl : k.castSucc < j
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rwa [j.succAbove_of_castSucc_lt, contractNth_apply_of_lt]

Premises used: Fin.succAbove_of_castSucc_lt, Fin.contractNth_apply_of_lt
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
h : (↑k : ℕ) < (↑j : ℕ)
inl inl₁ inl₂ inl₃ : (↑k.castSucc : ℕ) < (↑j : ℕ)
⊢ k.castSucc < j

Tactic:
rwa [Fin.lt_def]

Premises used: Fin.lt_def
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
h : (↑k : ℕ) = (↑j : ℕ)
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
False.elim (hjk h.symm)

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
h : (↑k : ℕ) = (↑j : ℕ)
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
exact False.elim (hjk h.symm)

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
h : (↑j : ℕ) < (↑k : ℕ)
inr : j ≤ k.castSucc
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]

Premises used: Fin.succAbove_of_le_castSucc, Fin.contractNth_apply_of_gt
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
h : (↑j : ℕ) < (↑k : ℕ)
⊢ j ≤ k.castSucc

Tactic:
Fin.le_iff_val_le_val.2 (le_of_lt h)

Premises used: Iff.mpr, le_of_lt, Fin.le_iff_val_le_val
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
h : (↑j : ℕ) < (↑k : ℕ)
⊢ j ≤ k.castSucc

Tactic:
exact Fin.le_iff_val_le_val.2 (le_of_lt h)

Premises used: Iff.mpr, le_of_lt, Fin.le_iff_val_le_val
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
h : ∀ (x : Fin n), (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
⊢ f ∘ j.contractNth opα g = j.contractNth opβ (f ∘ g)

Tactic:
ext x
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ∀ (h : (↑x : ℕ) < (↑j : ℕ)), (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
h₁ : ∀ (h : (↑x : ℕ) = (↑j : ℕ)), (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
h₂ : ∀ (h : (↑j : ℕ) < (↑x : ℕ)), (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
rcases lt_trichotomy (x : ℕ) j with (h | h | h)

Premises used: Fin.val, lt_trichotomy
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : (↑x : ℕ) < (↑j : ℕ)
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
simp only [Function.comp_apply, contractNth_apply_of_lt, h]

Premises used: Function.comp_apply, Fin.contractNth_apply_of_lt
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : (↑x : ℕ) = (↑j : ℕ)
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
simp only [Function.comp_apply, contractNth_apply_of_eq, h, hf]

Premises used: Function.comp_apply, Fin.contractNth_apply_of_eq
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : (↑j : ℕ) < (↑x : ℕ)
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
simp only [Function.comp_apply, contractNth_apply_of_gt, h]

Premises used: Fin.contractNth_apply_of_gt, Function.comp_apply
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : ai = bi
h :
  Eq.{u_1 + 1} (α :=
    Fin (Sigma.fst (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)) → α)
    (Sigma.snd (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a) :
      Fin (Sigma.fst (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)) → α)
    (Sigma.snd (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) bi b) ∘ Fin.cast hi :
      Fin (Sigma.fst (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)) → α)
subst :
  ∀ (b : Fin ai → α)
    (h :
      Eq.{u_1 + 1} (α :=
        Fin (Sigma.fst (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)) → α)
        (Sigma.snd (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a) :
          Fin (Sigma.fst (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)) → α)
        (Sigma.snd (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai b) ∘ Fin.cast ⋯ :
          Fin (Sigma.fst (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)) → α)),
    Eq.{u_1 + 1} (α := (ii : ℕ) × (Fin ii → α)) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)
      (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai b)
⊢ Eq.{u_1 + 1} (α := (ii : ℕ) × (Fin ii → α)) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)
    (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) bi b)

Tactic:
subst hi
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Type u_1
ai : ℕ
a b : Fin ai → α
h :
  Eq.{u_1 + 1} (α :=
    Fin (Sigma.fst (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)) → α)
    (Sigma.snd (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a) :
      Fin (Sigma.fst (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)) → α)
    (Sigma.snd (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai b) ∘ Fin.cast ⋯ :
      Fin (Sigma.fst (β := fun (ii : ℕ) ↦ Fin ii → α) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)) → α)
⊢ Eq.{u_1 + 1} (α := (ii : ℕ) × (Fin ii → α)) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)
    (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai b)

Tactic:
simpa using h
-- Module: Mathlib.Data.Fin.Tuple.Basic
Goal:
α : Type u_1
a b : (ii : ℕ) × (Fin ii → α)
⊢ a = b ↔
    ∃ (h : a.fst (β := fun (ii : ℕ) ↦ Fin ii → α) = b.fst (β := fun (ii : ℕ) ↦ Fin ii → α)),
      a.snd (β := fun (ii : ℕ) ↦ Fin ii → α) = b.snd (β := fun (ii : ℕ) ↦ Fin ii → α) ∘ Fin.cast h

Tactic:
⟨fun h ↦ h ▸ ⟨rfl, funext <| Fin.rec fun _ _ ↦ rfl⟩, fun ⟨_, h'⟩ ↦
    sigma_eq_of_eq_comp_cast _ h'⟩

Premises used: Eq.rec, Fin.rec, Fin.sigma_eq_of_eq_comp_cast, funext, Iff.intro, Exists.intro, _private.0.Fin.sigma_eq_iff_eq_comp_cast.match_1, Eq, rfl
-- Module: Mathlib.Data.Fin.Tuple.BubbleSortInduction
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j →
      (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i →
        P (f ∘ (⇑σ : (a : Fin n) → Fin n)) →
          P (f ∘ Function.comp (β := Fin n) (⇑σ : (a : Fin n) → Fin n) (⇑(Equiv.swap i j) : (a : Fin n) → Fin n))
letI : P (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))
⊢ P (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
letI := @Preorder.lift _ (Lex (Fin n → α)) _ fun σ : Equiv.Perm (Fin n) => toLex (f ∘ σ)
-- Module: Mathlib.Data.Fin.Tuple.BubbleSortInduction
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j →
      (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i →
        P (f ∘ (⇑σ : (a : Fin n) → Fin n)) →
          P (f ∘ Function.comp (β := Fin n) (⇑σ : (a : Fin n) → Fin n) (⇑(Equiv.swap i j) : (a : Fin n) → Fin n))
this : Preorder (Equiv.Perm (Fin n)) :=
  Preorder.lift.{0, u_1} (β := Lex (Fin n → α)) fun (σ : Equiv.Perm (Fin n)) ↦
    (toLex : (a : Fin n → α) → Lex (Fin n → α)) (f ∘ (⇑σ : (a : Fin n) → Fin n))
⊢ P (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
@WellFounded.induction_bot' _ _ _ (IsWellFounded.wf : WellFounded (· < ·))
      (Equiv.refl _) (sort f) P (fun σ => f ∘ σ) (fun σ hσ hfσ => ?_) hf

Premises used: WellFounded.induction_bot', IsWellFounded.wf
-- Module: Mathlib.Data.Fin.Tuple.BubbleSortInduction
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j →
      (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i →
        P (f ∘ (⇑σ : (a : Fin n) → Fin n)) →
          P (f ∘ Function.comp (β := Fin n) (⇑σ : (a : Fin n) → Fin n) (⇑(Equiv.swap i j) : (a : Fin n) → Fin n))
this : Preorder (Equiv.Perm (Fin n)) :=
  Preorder.lift.{0, u_1} (β := Lex (Fin n → α)) fun (σ : Equiv.Perm (Fin n)) ↦
    (toLex : (a : Fin n → α) → Lex (Fin n → α)) (f ∘ (⇑σ : (a : Fin n) → Fin n))
_ :
  ∀ (σ : Fin n ≃ Fin n)
    (hσ :
      Ne.{u_1 + 1} (α := Fin n → α) ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) σ)
        ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) (sort f)))
    (hfσ : P ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) σ)),
    ∃ c < σ, P ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) c)
⊢ P (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
refine
    @WellFounded.induction_bot' _ _ _ (IsWellFounded.wf : WellFounded (· < ·))
      (Equiv.refl _) (sort f) P (fun σ => f ∘ σ) (fun σ hσ hfσ => ?_) hf

Premises used: WellFounded.induction_bot', IsWellFounded.wf
-- Module: Mathlib.Data.Fin.Tuple.BubbleSortInduction
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j →
      (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i →
        P (f ∘ (⇑σ : (a : Fin n) → Fin n)) →
          P (f ∘ Function.comp (β := Fin n) (⇑σ : (a : Fin n) → Fin n) (⇑(Equiv.swap i j) : (a : Fin n) → Fin n))
this : Preorder (Equiv.Perm (Fin n)) :=
  Preorder.lift.{0, u_1} (β := Lex (Fin n → α)) fun (σ : Equiv.Perm (Fin n)) ↦
    (toLex : (a : Fin n → α) → Lex (Fin n → α)) (f ∘ (⇑σ : (a : Fin n) → Fin n))
σ : Fin n ≃ Fin n
hσ :
  Ne.{u_1 + 1} (α := Fin n → α) ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) σ)
    ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) (sort f))
hfσ : P ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) σ)
obtain :
  ∀ (i j : Fin n) (hij₁ : i < j) (hij₂ : (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i),
    ∃ c < σ, P ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) c)
⊢ ∃ c < σ, P ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) c)

Tactic:
obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ

Premises used: Tuple.antitone_pair_of_not_sorted'
-- Module: Mathlib.Data.Fin.Tuple.BubbleSortInduction
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j →
      (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i →
        P (f ∘ (⇑σ : (a : Fin n) → Fin n)) →
          P (f ∘ Function.comp (β := Fin n) (⇑σ : (a : Fin n) → Fin n) (⇑(Equiv.swap i j) : (a : Fin n) → Fin n))
this : Preorder (Equiv.Perm (Fin n)) :=
  Preorder.lift.{0, u_1} (β := Lex (Fin n → α)) fun (σ : Equiv.Perm (Fin n)) ↦
    (toLex : (a : Fin n → α) → Lex (Fin n → α)) (f ∘ (⇑σ : (a : Fin n) → Fin n))
σ : Fin n ≃ Fin n
hσ :
  Ne.{u_1 + 1} (α := Fin n → α) ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) σ)
    ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) (sort f))
hfσ : P ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) σ)
i j : Fin n
hij₁ : i < j
hij₂ : (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i
⊢ ∃ c < σ, P ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) c)

Tactic:
⟨σ * Equiv.swap i j, Pi.lex_desc hij₁.le hij₂, h σ i j hij₁ hij₂ hfσ⟩

Premises used: HMul.hMul, Equiv.swap, Pi.lex_desc, LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.Data.Fin.Tuple.BubbleSortInduction
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j →
      (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i →
        P (f ∘ (⇑σ : (a : Fin n) → Fin n)) →
          P (f ∘ Function.comp (β := Fin n) (⇑σ : (a : Fin n) → Fin n) (⇑(Equiv.swap i j) : (a : Fin n) → Fin n))
this : Preorder (Equiv.Perm (Fin n)) :=
  Preorder.lift.{0, u_1} (β := Lex (Fin n → α)) fun (σ : Equiv.Perm (Fin n)) ↦
    (toLex : (a : Fin n → α) → Lex (Fin n → α)) (f ∘ (⇑σ : (a : Fin n) → Fin n))
σ : Fin n ≃ Fin n
hσ :
  Ne.{u_1 + 1} (α := Fin n → α) ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) σ)
    ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) (sort f))
hfσ : P ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) σ)
i j : Fin n
hij₁ : i < j
hij₂ : (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i
⊢ ∃ c < σ, P ((fun (σ : Fin n ≃ Fin n) ↦ (f ∘ (⇑σ : (a : Fin n) → Fin n) : Fin n → α)) c)

Tactic:
exact ⟨σ * Equiv.swap i j, Pi.lex_desc hij₁.le hij₂, h σ i j hij₁ hij₂ hfσ⟩
-- Module: Mathlib.Data.Fin.Tuple.BubbleSortInduction
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
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) : (a : Fin n) → Fin n))
⊢ P (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
bubble_sort_induction' hf fun _ => h _

Premises used: Function.comp, Tuple.bubble_sort_induction', DFunLike.coe
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
n : ℕ
α : Type u
p : Fin n → Type u
τ : Type u
f : FromTypes (vecCons α p) τ
a : α
args : (i : Fin n) → p i
⊢ f.uncurry (p := vecCons α p) (Fin.cons (α := vecCons α p) a args) = (f a).uncurry (p := p) args

Tactic:
rfl

Premises used: Eq.mpr, Function.FromTypes.uncurry, Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, Nat.mod, Fin.cases, Matrix.vecTail, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
n : ℕ
p : Fin (n + 1) → Type u
τ : Type u
f : FromTypes p τ
args : (i : Fin (n + 1)) → p i
⊢ f.uncurry (p := p) args = (f (args 0)).uncurry (p := vecTail p) (Fin.tail (α := p) args)

Tactic:
rfl

Premises used: Function.FromTypes.uncurry, Fin.tail, rfl
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
n : ℕ
α : Type u
p : Fin n → Type u
τ : Type u
f : ((i : Fin (n + 1)) → vecCons α p i) → τ
a : α
⊢ curry (p := vecCons α p) f a =
    curry (p := p)
      (dcomp (β := fun {x : (i : Fin n) → vecCons α p i.succ} ↦ (i : Fin (n + 1)) → vecCons α p i) (φ :=
        fun {x : (i : Fin n) → vecCons α p i.succ} (y : (i : Fin (n + 1)) → vecCons α p i) ↦ τ)
        (fun {x : (i : Fin n) → vecCons α p i.succ} ↦ f) (Fin.cons (α := vecCons α p) a))

Tactic:
rfl

Premises used: Fin.cons, Fin.induction.go, Fin.induction, Function.FromTypes.curry, Fin.cases, Matrix.vecTail, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
n : ℕ
p : Fin (n + 1) → Type u
τ : Type u
f : ((i : Fin (n + 1)) → p i) → τ
a : p 0
⊢ curry (p := p) f a = curry (p := fun (i : Fin n) ↦ p i.succ) (f ∘ Fin.cons (α := p) a)

Tactic:
rfl

Premises used: Function.FromTypes.curry, Matrix.vecTail, rfl
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
τ : Type u
p : Fin 0 → Type u
f : FromTypes p τ
⊢ curry (p := p) (f.uncurry (p := p)) = f

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
τ : Type u
n : ℕ
ih : ∀ {p : Fin n → Type u} (f : FromTypes p τ), curry (p := p) (f.uncurry (p := p)) = f
p : Fin (n + 1) → Type u
f : FromTypes p τ
⊢ curry (p := p) (f.uncurry (p := p)) = f

Tactic:
funext (ih <| f ·)

Premises used: Function.FromTypes, funext
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
τ : Type u
n : ℕ
ih : ∀ {p : Fin n → Type u} (f : FromTypes p τ), curry (p := p) (f.uncurry (p := p)) = f
p : Fin (n + 1) → Type u
f : FromTypes p τ
⊢ curry (p := p) (f.uncurry (p := p)) = f

Tactic:
exact funext (ih <| f ·)

Premises used: funext
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
n : ℕ
p : Fin n → Type u
τ : Type u
f : FromTypes p τ
zero : ∀ {p : Fin 0 → Type u} (f : FromTypes p τ), curry (p := p) (f.uncurry (p := p)) = f
succ :
  ∀ (n : ℕ) (ih : ∀ {p : Fin n → Type u} (f : FromTypes p τ), curry (p := p) (f.uncurry (p := p)) = f)
    {p : Fin (n + 1) → Type u} (f : FromTypes p τ), curry (p := p) (f.uncurry (p := p)) = f
⊢ curry (p := p) (f.uncurry (p := p)) = f

Tactic:
induction n with
  | zero => rfl
  | succ n ih => exact funext (ih <| f ·)
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
h : ∀ (args : (i : Fin n) → p i), (curry (p := p) f).uncurry (p := p) args = f args
⊢ (curry (p := p) f).uncurry (p := p) = f

Tactic:
ext args
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
τ : Type u
p : Fin 0 → Type u
f : ((i : Fin 0) → p i) → τ
args : (i : Fin 0) → p i
⊢ (curry (p := p) f).uncurry (p := p) args = f args

Tactic:
congrArg f (Subsingleton.allEq _ _)

Premises used: Function.FromTypes.uncurry, congrArg, Subsingleton.allEq, Function.FromTypes.curry
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
τ : Type u
p : Fin 0 → Type u
f : ((i : Fin 0) → p i) → τ
args : (i : Fin 0) → p i
⊢ (curry (p := p) f).uncurry (p := p) args = f args

Tactic:
exact congrArg f (Subsingleton.allEq _ _)

Premises used: congrArg, Subsingleton.allEq