awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
⊢ 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)
have 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)
Tactic: simp_rw [find?_eq_dite, decide_eq_true_eq]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
⊢ (find? p).get ⋯ = Fin.find (fun (x : Fin n) ↦ p x = true) ⋯
have 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) sorry =
  Fin.find (fun (x : Fin n) ↦ p x = true) sorry
Tactic: simp_rw [find?_eq_dite, Option.get_dite]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : Fin n → Prop
inst : DecidablePred p
h : ∃ (i : Fin n), p i
⊢ Option.get (find? fun (x : Fin n) ↦ decide (p x)) ⋯ = Fin.find p h
have simp_rw : Option.get (if h : ∃ (i : Fin n), p i then some (Fin.find p h) else none) sorry = Fin.find p h
Tactic: simp_rw [find?_decide_eq_dite, Option.get_dite]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : Fin n → Bool
h : ∃ (i : Fin n), p i = true
⊢ find? p = some (Fin.find (fun (x : Fin n) ↦ p x = true) h)
have 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)
Tactic: simp_rw [find?_eq_dite, h, dite_true]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
⊢ find? p = some (Fin.find (fun (x : Fin n) ↦ p x = true) h)
have simp_rw₁ : (if h_1 : True then some (Fin.find (fun (x : Fin n) ↦ p x = true) sorry) else none) =
  some (Fin.find (fun (x : Fin n) ↦ p x = true) h)
Tactic: simp_rw [find?_eq_dite, h, dite_true]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
p : Fin n → Bool
h : (find? p).isSome = true
⊢ find? p = some (Fin.find (fun (x : Fin n) ↦ p x = true) ⋯)
have 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) sorry)
Tactic: simp_rw [find?_eq_dite, exists_eq_true_of_isSome_find? h, dite_true]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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) ⋯)
⊢ find? p = some (Fin.find (fun (x : Fin n) ↦ p x = true) ⋯)
have simp_rw₁ : (if h_1 : True then some (Fin.find (fun (x : Fin n) ↦ p x = true) sorry) else none) =
  some (Fin.find (fun (x : Fin n) ↦ p x = true) sorry)
Tactic: simp_rw [find?_eq_dite, exists_eq_true_of_isSome_find? h, dite_true]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
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 = op (g k.castSucc) (g k.succ)
have this : ¬(↑k : ℕ) < (↑j : ℕ)
Tactic: have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : (↑k : ℕ) = (↑j : ℕ)
this : ¬(↑k : ℕ) < (↑j : ℕ)
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)
have 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)
Tactic: rw [contractNth, if_neg this, if_pos h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)
have rw₁ : (if (↑k : ℕ) = (↑j : ℕ) then op (g k.castSucc) (g k.succ) else g k.succ) = op (g k.castSucc) (g k.succ)
Tactic: rw [contractNth, if_neg this, if_pos h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)
have rw₂ : op (g k.castSucc) (g k.succ) = op (g k.castSucc) (g k.succ)
Tactic: rw [contractNth, if_neg this, if_pos h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : (↑j : ℕ) < (↑k : ℕ)
⊢ j.contractNth op g k = g k.succ
have 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
Tactic: rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ j.contractNth op g k = g k.succ
have rw₁ : (if (↑k : ℕ) = (↑j : ℕ) then op (g k.castSucc) (g k.succ) else g k.succ) = g k.succ
Tactic: rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ j.contractNth op g k = g k.succ
have rw₂ : g k.succ = g k.succ
Tactic: rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
⊢ j.contractNth op g k = g (j.succAbove k)
have inl : ∀ (h : (↑k : ℕ) < (↑j : ℕ)), j.contractNth op g k = g (j.succAbove k)
Tactic: rcases lt_trichotomy (k : ℕ) j with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
⊢ j.contractNth op g k = g (j.succAbove k)
have inr : ∀ (h : (↑k : ℕ) = (↑j : ℕ)), j.contractNth op g k = g (j.succAbove k)
Tactic: rcases lt_trichotomy (k : ℕ) j with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
⊢ j.contractNth op g k = g (j.succAbove k)
have inr₁ : ∀ (h : (↑j : ℕ) < (↑k : ℕ)), j.contractNth op g k = g (j.succAbove k)
Tactic: rcases lt_trichotomy (k : ℕ) j with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)
have inl : k.castSucc < j
Tactic: rwa [j.succAbove_of_castSucc_lt, contractNth_apply_of_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
h : (↑k : ℕ) < (↑j : ℕ)
⊢ k.castSucc < j
have inl : (↑k.castSucc : ℕ) < (↑j : ℕ)
Tactic: rwa [Fin.lt_def]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : (↑j : ℕ) ≠ (↑k : ℕ)
h : (↑j : ℕ) < (↑k : ℕ)
⊢ j.contractNth op g k = g (j.succAbove k)
have inr : j ≤ k.castSucc
Tactic: rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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) → α
⊢ f ∘ j.contractNth opα g = j.contractNth opβ (f ∘ g)
have h : ∀ (x : Fin n), (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
have h : ∀ (h : (↑x : ℕ) < (↑j : ℕ)), (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
Tactic: rcases lt_trichotomy (x : ℕ) j with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
have h₁ : ∀ (h : (↑x : ℕ) = (↑j : ℕ)), (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
Tactic: rcases lt_trichotomy (x : ℕ) j with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
have h₂ : ∀ (h : (↑j : ℕ) < (↑x : ℕ)), (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
Tactic: rcases lt_trichotomy (x : ℕ) j with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
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)) → α)
⊢ Eq.{u_1 + 1} (α := (ii : ℕ) × (Fin ii → α)) (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) ai a)
    (Sigma.mk (β := fun (ii : ℕ) ↦ Fin ii → α) bi b)
have 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 sorry :
        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: subst hi
Cleared hypotheses: bi, b, hi, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.BubbleSortInduction (goal)
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))
have _ : ∀ (σ : 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)
Tactic: refine
    @WellFounded.induction_bot' _ _ _ (IsWellFounded.wf : WellFounded (· < ·))
      (Equiv.refl _) (sort f) P (fun σ => f ∘ σ) (fun σ hσ hfσ => ?_) hf
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.BubbleSortInduction (goal)
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)
have 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)
Tactic: obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Curry (goal)
Goal:
n : ℕ
p : Fin n → Type u
τ : Type u
f : FromTypes p τ
⊢ curry (p := p) (f.uncurry (p := p)) = f
have zero : ∀ {p : Fin 0 → Type u} (f : FromTypes p τ), curry (p := p) (f.uncurry (p := p)) = f
Tactic: induction n with
  | zero => rfl
  | succ n ih => exact funext (ih <| f ·)
Cleared hypotheses: n, p, f
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Curry (goal)
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
⊢ curry (p := p) (f.uncurry (p := p)) = f
have 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
Tactic: induction n with
  | zero => rfl
  | succ n ih => exact funext (ih <| f ·)
Cleared hypotheses: n, p, f
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Curry (goal)
Goal:
n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
⊢ (curry (p := p) f).uncurry (p := p) = f
have h : ∀ (args : (i : Fin n) → p i), (curry (p := p) f).uncurry (p := p) args = f args
Tactic: ext args
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Curry (goal)
Goal:
n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
args : (i : Fin n) → p i
⊢ (curry (p := p) f).uncurry (p := p) args = f args
have h : ∀ {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: induction n with
  | zero => exact congrArg f (Subsingleton.allEq _ _)
  | succ n ih => exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))
Cleared hypotheses: n, p, f, args
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Curry (goal)
Goal:
n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
args : (i : Fin n) → p i
h :
  ∀ {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
⊢ (curry (p := p) f).uncurry (p := p) args = f args
have h₁ : ∀ (n : ℕ)
  (ih :
    ∀ {p : Fin n → Type u} (f : ((i : Fin n) → p i) → τ) (args : (i : Fin n) → p i),
      (curry (p := p) f).uncurry (p := p) args = f args)
  {p : Fin (n + 1) → Type u} (f : ((i : Fin (n + 1)) → p i) → τ) (args : (i : Fin (n + 1)) → p i),
  (curry (p := p) f).uncurry (p := p) args = f args
Tactic: induction n with
  | zero => exact congrArg f (Subsingleton.allEq _ _)
  | succ n ih => exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))
Cleared hypotheses: n, p, f, args
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
i : Fin n
⊢ Eq (α := α) ((snoc x ha : (a : Fin (n + 1)) → α) i.castSucc : α) ((x : (a : Fin n) → α) i : α)
have rw : Eq (α := α) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ α) (⇑x : (a : Fin n) → α) a i.castSucc : α)
  ((x : (a : Fin n) → α) i : α)
Tactic: rw [coe_snoc, Fin.snoc_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
i : Fin n
rw :
  Eq (α := α) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ α) (⇑x : (a : Fin n) → α) a i.castSucc : α)
    ((x : (a : Fin n) → α) i : α)
⊢ Eq (α := α) ((snoc x ha : (a : Fin (n + 1)) → α) i.castSucc : α) ((x : (a : Fin n) → α) i : α)
have rw₁ : Eq (α := α) ((x : (a : Fin n) → α) i : α) ((x : (a : Fin n) → α) i : α)
Tactic: rw [coe_snoc, Fin.snoc_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
⊢ (snoc x ha : (a : Fin (n + 1)) → α) (last n) = a
have rw : Fin.snoc (α := fun (a : Fin (n + 1)) ↦ α) (⇑x : (a : Fin n) → α) a (last n) = a
Tactic: rw [coe_snoc, Fin.snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
rw : Fin.snoc (α := fun (a : Fin (n + 1)) ↦ α) (⇑x : (a : Fin n) → α) a (last n) = a
⊢ (snoc x ha : (a : Fin (n + 1)) → α) (last n) = a
have rw₁ : a = a
Tactic: rw [coe_snoc, Fin.snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
⊢ i = j
have pos : ∀ (hi : i = 0), i = j
Tactic: by_cases hi : i = 0
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
pos : ∀ (hi : i = 0), i = j
⊢ i = j
have neg : ∀ (hi : ¬i = 0), i = j
Tactic: by_cases hi : i = 0
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : i = 0
⊢ i = j
have pos : ∀ (hj : j = 0), i = j
Tactic: by_cases hj : j = 0
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : i = 0
pos : ∀ (hj : j = 0), i = j
⊢ i = j
have neg : ∀ (hj : ¬j = 0), i = j
Tactic: by_cases hj : j = 0
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (hypothesis)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : i = 0
hj : ¬j = 0
⊢ i = j
have hij₁ : a = b
Tactic: simp only [if_pos hi, eq_one_of_ne_zero j hj,
          if_neg (Ne.symm Fin.zero_ne_one)] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : ¬i = 0
⊢ i = j
have neg : ∀
  (hij :
    Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) 1) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j))
  (hi : ¬i = 0), 1 = j
Tactic: rw [eq_one_of_ne_zero i hi] at hij ⊢
Cleared hypotheses: hij, hi
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) 1) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : ¬i = 0
⊢ 1 = j
have pos : ∀ (hj : j = 0), 1 = j
Tactic: by_cases hj : j = 0