awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
h : n = m
⊢ (castOrderIso h).symm = castOrderIso ⋯
have subst : (castOrderIso sorry).symm = castOrderIso sorry
Tactic: subst h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
h : n = n
⊢ castOrderIso h = OrderIso.refl (Fin n)
have h₁ : ∀ (x : Fin n),
  (↑((castOrderIso h : (a : Fin n) → Fin n) x) : ℕ) = (↑((OrderIso.refl (Fin n) : (a : Fin n) → Fin n) x) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
h : n = m
⊢ (castOrderIso h).toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin m) ↦ x1 ≤ x2) = Equiv.cast ⋯
have subst : (castOrderIso sorry).toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) = Equiv.cast sorry
Tactic: subst h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : Fin n
⊢ (↑((e : (a : Fin n) → Fin m) i) : ℕ) = (↑i : ℕ)
have rcases : ∀ (i : ℕ) (hi : i < n), (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = (↑(⟨i, hi⟩ : Fin n) : ℕ)
Tactic: rcases i with ⟨i, hi⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = (↑(⟨i, hi⟩ : Fin n) : ℕ)
have dsimp : (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i
have h : ∀ (i : ℕ) (h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1)
  (hi : i < n), (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i
Tactic: induction i using Nat.strong_induction_on with | _ i h
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
⊢ (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i
have h₁ : ∀ (j : ℕ) (hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)), j < i
Tactic: refine le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_)
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
h₁ : ∀ (j : ℕ) (hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)), j < i
⊢ (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i
have h₂ : ∀ (j : ℕ) (hj : j < i), j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
Tactic: refine le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_)
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (hypothesis)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
j : ℕ
hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
⊢ j < i
have this : (e.symm : (a : Fin m) → Fin n) ⟨j, sorry⟩ < (⟨i, hi⟩ : Fin n)
Tactic: have := e.symm.lt_symm_apply.1 (mk_lt_of_lt_val hj)
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (hypothesis)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
j : ℕ
hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
this : (e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩ < (⟨i, hi⟩ : Fin n)
⊢ j < i
have h₁ : (↑((e : (a : Fin n) → Fin m) (⟨(↑((e.symm : (a : Fin m) → Fin n) (⟨j, sorry⟩ : Fin m)) : ℕ), sorry⟩ : Fin n)) : ℕ) =
  (↑((e.symm : (a : Fin m) → Fin n) ⟨j, sorry⟩) : ℕ)
Tactic: specialize h _ this (e.symm _).is_lt
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (hypothesis)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
j : ℕ
hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
this : (e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩ < (⟨i, hi⟩ : Fin n)
h :
  (↑((e : (a : Fin n) → Fin m) (⟨(↑((e.symm : (a : Fin m) → Fin n) (⟨j, ⋯⟩ : Fin m)) : ℕ), ⋯⟩ : Fin n)) : ℕ) =
    (↑((e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩) : ℕ)
⊢ j < i
have h₁ : j = (↑((e.symm : (a : Fin m) → Fin n) ⟨j, sorry⟩) : ℕ)
Tactic: simp only [Fin.eta, OrderIso.apply_symm_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
j : ℕ
hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
this : (e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩ < (⟨i, hi⟩ : Fin n)
h : j = (↑((e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩) : ℕ)
⊢ j < i
have h₁ : (↑((e.symm : (a : Fin m) → Fin n) (⟨j, sorry⟩ : Fin m)) : ℕ) < i
Tactic: rwa [h]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
have h₁ : (↑((e : (a : Fin n) → Fin m) (⟨j, sorry⟩ : Fin n)) : ℕ) < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
Tactic: rwa [← h j hj (hj.trans hi), ← lt_def, e.lt_iff_lt]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
j : ℕ
hj : j < i
h₁ : (↑((e : (a : Fin n) → Fin m) (⟨j, ⋯⟩ : Fin n)) : ℕ) < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
⊢ j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
have h₂ : LT.lt (α := Fin m) ((e : (a : Fin n) → Fin m) ⟨j, sorry⟩ : Fin m) ((e : (a : Fin n) → Fin m) ⟨i, hi⟩ : Fin m)
Tactic: rwa [← h j hj (hj.trans hi), ← lt_def, e.lt_iff_lt]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
j : ℕ
hj : j < i
h₁ : (↑((e : (a : Fin n) → Fin m) (⟨j, ⋯⟩ : Fin n)) : ℕ) < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
h₂ : LT.lt (α := Fin m) ((e : (a : Fin n) → Fin m) ⟨j, ⋯⟩ : Fin m) ((e : (a : Fin n) → Fin m) ⟨i, hi⟩ : Fin m)
⊢ j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
have h₃ : (⟨j, sorry⟩ : Fin n) < ⟨i, hi⟩
Tactic: rwa [← h j hj (hj.trans hi), ← lt_def, e.lt_iff_lt]
-- Lean 4 proof step from Mathlib.Order.Fin.Clamp (goal)
Goal:
n m : ℕ
hmn : m ≤ n
⊢ clamp n m = last m
have h : (↑(clamp n m) : ℕ) = (↑(last m) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Fin.Finset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
x_1 : ↥{a, b}
x : α
hx : Membership.mem (γ := Finset α) {a, b} x
⊢ ∃ (a_1 : Fin 2),
    ![Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) a ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) b ⋯]
        a_1 =
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) x hx
have hx₁ : x = a ∨ x = b
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton] at hx
-- Lean 4 proof step from Mathlib.Order.Fin.Finset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
x_1 : ↥{a, b}
x : α
hx_1 : Membership.mem (γ := Finset α) {a, b} x
hx : x = a ∨ x = b
⊢ ∃ (a_1 : Fin 2),
    ![Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) a ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) b ⋯]
        a_1 =
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) x hx_1
have inl : ∀ (hab : x < b) (x_2 : ↥{x, b}) (hx : Membership.mem (γ := Finset α) {x, b} x),
  ∃ (a : Fin 2),
    ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_3) x sorry,
          Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_3) b sorry]
        a =
      Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_3) x hx
Tactic: obtain rfl | rfl := hx
Cleared hypotheses: a, hab, x_1, hx_1, hx
-- Lean 4 proof step from Mathlib.Order.Fin.Finset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
x_1 : ↥{a, b}
x : α
hx_1 : Membership.mem (γ := Finset α) {a, b} x
hx : x = a ∨ x = b
inl :
  ∀ (hab : x < b) (x_2 : ↥{x, b}) (hx : Membership.mem (γ := Finset α) {x, b} x),
    ∃ (a : Fin 2),
      ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_3) x ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_3) b ⋯]
          a =
        Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_3) x hx
⊢ ∃ (a_1 : Fin 2),
    ![Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) a ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) b ⋯]
        a_1 =
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) x hx_1
have inr : ∀ (hab : a < x) (x_2 : ↥{a, x}) (hx : Membership.mem (γ := Finset α) {a, x} x),
  ∃ (a_1 : Fin 2),
    ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_3) a sorry,
          Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_3) x sorry]
        a_1 =
      Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_3) x hx
Tactic: obtain rfl | rfl := hx
Cleared hypotheses: b, hab, x_1, hx_1, hx
-- Lean 4 proof step from Mathlib.Order.Fin.Finset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x_1 : ↥{a, b, c}
x : α
hx : Membership.mem (γ := Finset α) {a, b, c} x
⊢ ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) a ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) b ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) c ⋯]
        a_1 =
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) x hx
have hx₁ : x = a ∨ x = b ∨ x = c
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton] at hx
-- Lean 4 proof step from Mathlib.Order.Fin.Finset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x_1 : ↥{a, b, c}
x : α
hx_1 : Membership.mem (γ := Finset α) {a, b, c} x
hx : x = a ∨ x = b ∨ x = c
⊢ ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) a ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) b ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) c ⋯]
        a_1 =
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) x hx_1
have inl : ∀ (hab : x < b) (x_2 : ↥{x, b, c}) (hx : Membership.mem (γ := Finset α) {x, b, c} x),
  ∃ (a : Fin 3),
    ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) x sorry,
          Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) b sorry,
          Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) c sorry]
        a =
      Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) x hx
Tactic: obtain rfl | rfl | rfl := hx
Cleared hypotheses: a, hab, x_1, hx_1, hx
-- Lean 4 proof step from Mathlib.Order.Fin.Finset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x_1 : ↥{a, b, c}
x : α
hx_1 : Membership.mem (γ := Finset α) {a, b, c} x
hx : x = a ∨ x = b ∨ x = c
inl :
  ∀ (hab : x < b) (x_2 : ↥{x, b, c}) (hx : Membership.mem (γ := Finset α) {x, b, c} x),
    ∃ (a : Fin 3),
      ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) x ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) b ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) c ⋯]
          a =
        Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) x hx
⊢ ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) a ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) b ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) c ⋯]
        a_1 =
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) x hx_1
have inr : ∀ (hab : a < x) (hbc : x < c) (x_2 : ↥{a, x, c}) (hx : Membership.mem (γ := Finset α) {a, x, c} x),
  ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) a sorry,
          Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) x sorry,
          Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) c sorry]
        a_1 =
      Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) x hx
Tactic: obtain rfl | rfl | rfl := hx
Cleared hypotheses: b, hab, hbc, x_1, hx_1, hx
-- Lean 4 proof step from Mathlib.Order.Fin.Finset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x_1 : ↥{a, b, c}
x : α
hx_1 : Membership.mem (γ := Finset α) {a, b, c} x
hx : x = a ∨ x = b ∨ x = c
inl :
  ∀ (hab : x < b) (x_2 : ↥{x, b, c}) (hx : Membership.mem (γ := Finset α) {x, b, c} x),
    ∃ (a : Fin 3),
      ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) x ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) b ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) c ⋯]
          a =
        Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) x hx
inr :
  ∀ (hab : a < x) (hbc : x < c) (x_2 : ↥{a, x, c}) (hx : Membership.mem (γ := Finset α) {a, x, c} x),
    ∃ (a_1 : Fin 3),
      ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) a ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) x ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) c ⋯]
          a_1 =
        Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) x hx
⊢ ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) a ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) b ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) c ⋯]
        a_1 =
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) x hx_1
have inr₁ : ∀ (hbc : b < x) (x_2 : ↥{a, b, x}) (hx : Membership.mem (γ := Finset α) {a, b, x} x),
  ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_3) a sorry,
          Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_3) b sorry,
          Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_3) x sorry]
        a_1 =
      Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_3) x hx
Tactic: obtain rfl | rfl | rfl := hx
Cleared hypotheses: c, hbc, x_1, hx_1, hx
-- Lean 4 proof step from Mathlib.Order.Fin.SuccAboveOrderIso (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Function.Bijective (β := ↥{i}ᶜ) fun (a : Fin (n + 1)) ↦
    Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
      ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯
have left : Function.Injective (β := ↥{i}ᶜ) fun (a : Fin (n + 1)) ↦
  Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
    ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Fin.SuccAboveOrderIso (goal)
Goal:
n : ℕ
i : Fin (n + 2)
left :
  Function.Injective (β := ↥{i}ᶜ) fun (a : Fin (n + 1)) ↦
    Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
      ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯
⊢ Function.Bijective (β := ↥{i}ᶜ) fun (a : Fin (n + 1)) ↦
    Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
      ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯
have right : Function.Surjective (β := ↥{i}ᶜ) fun (a : Fin (n + 1)) ↦
  Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
    ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Fin.SuccAboveOrderIso (hypothesis)
Goal:
n : ℕ
i j : Fin (n + 2)
hj : Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ j
⊢ ∃ (a : Fin (n + 1)),
    (fun (a : Fin (n + 1)) ↦
          (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
              ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
            ↥{i}ᶜ))
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x) j hj
have hj₁ : ¬j = i
Tactic: simp only [mem_compl, mem_singleton] at hj
-- Lean 4 proof step from Mathlib.Order.Fin.SuccAboveOrderIso (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hj_1 : Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ j
hj : ¬j = i
⊢ ∃ (a : Fin (n + 1)),
    (fun (a : Fin (n + 1)) ↦
          (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
              ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
            ↥{i}ᶜ))
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x) j hj_1
have right : ∀ (hj : Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ j) (hj_2 : ¬j = 0),
  ∃ (a : Fin (n + 1)),
    (fun (a : Fin (n + 1)) ↦
          (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x)
              ((succAboveOrderEmb 0 : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) sorry :
            ↥{0}ᶜ))
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x) j hj
Tactic: obtain rfl | ⟨i, rfl⟩ := Fin.eq_zero_or_eq_succ i
Cleared hypotheses: i, hj_1, hj
-- Lean 4 proof step from Mathlib.Order.Fin.SuccAboveOrderIso (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hj_1 : Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ j
hj : ¬j = i
right :
  ∀ (hj : Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ j) (hj_2 : ¬j = 0),
    ∃ (a : Fin (n + 1)),
      (fun (a : Fin (n + 1)) ↦
            (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x)
                ((succAboveOrderEmb 0 : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
              ↥{0}ᶜ))
          a =
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x) j hj
⊢ ∃ (a : Fin (n + 1)),
    (fun (a : Fin (n + 1)) ↦
          (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
              ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
            ↥{i}ᶜ))
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x) j hj_1
have right₁ : ∀ (i : Fin (n + 1)) (hj : Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ j) (hj_2 : ¬j = i.succ),
  ∃ (a : Fin (n + 1)),
    (fun (a : Fin (n + 1)) ↦
          (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ x)
              ((i.succ.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) sorry :
            ↥{i.succ}ᶜ))
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ x) j hj
Tactic: obtain rfl | ⟨i, rfl⟩ := Fin.eq_zero_or_eq_succ i
Cleared hypotheses: i, hj_1, hj
-- Lean 4 proof step from Mathlib.Order.Fin.Tuple (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ Pi.Lex (β := α) (fun (x1 x2 : Fin n.succ) ↦ x1 < x2) (@s) (cons (α := α) x₀ x) (cons (α := α) y₀ y) ↔
    s x₀ y₀ ∨
      x₀ = y₀ ∧ Pi.Lex (β := fun (i : Fin n) ↦ α i.succ) (fun (x1 x2 : Fin n) ↦ x1 < x2) (fun (i : Fin n) ↦ s) x y
have simp_rw : (((LT.lt (α := Fin n.succ) 0 0 → Eq (α := α 0) (cons (α := α) x₀ x 0) (cons (α := α) y₀ y 0)) ∧
        ∀ (i : Fin n), i.succ < 0 → Eq (α := α i.succ) (cons (α := α) x₀ x i.succ) (cons (α := α) y₀ y i.succ)) ∧
      s x₀ y₀ ∨
    ∃ (i : Fin n),
      ((0 < i.succ → Eq (α := α 0) (cons (α := α) x₀ x 0) (cons (α := α) y₀ y 0)) ∧
          ∀ (i_1 : Fin n),
            i_1.succ < i.succ → Eq (α := α i_1.succ) (cons (α := α) x₀ x i_1.succ) (cons (α := α) y₀ y i_1.succ)) ∧
        s (x i) (y i)) ↔
  s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ (i : Fin n), (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
Tactic: simp_rw [Pi.Lex, Fin.exists_fin_succ, Fin.cons_succ, Fin.cons_zero, Fin.forall_iff_succ]
-- Lean 4 proof step from Mathlib.Order.Fin.Tuple (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Type u_2
inst : (i : Fin (n + 1)) → LE (α i)
⊢ Eq (α := α 0 × ((i : Fin n) → α (succAbove 0 i)) ≃o ((i : Fin (n + 1)) → α i)) (insertNthOrderIso α 0)
    (consOrderIso α)
have h : ∀ (x : α 0 × ((i : Fin n) → α (succAbove 0 i))) (x_1 : Fin (n + 1)),
  Eq (α := α x_1)
    ((insertNthOrderIso α 0 : (a : α 0 × ((i : Fin n) → α (succAbove 0 i))) → (i : Fin (n + 1)) → α i) x x_1 : α x_1)
    ((consOrderIso α : (a : α 0 × ((i : Fin n) → α (succAbove 0 i))) → (i : Fin (n + 1)) → α i) x x_1 : α x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Fin.Tuple (goal)
Goal:
n : ℕ
α : Type u_2
inst : LE α
⊢ Eq.{u_2 + 1} (α := α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α))
    (insertNthOrderIso.{u_2} (fun (x : Fin (n + 1)) ↦ α) (last n) : α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α))
    (snocOrderIso.{u_2} (n := n) fun (x : Fin (n + 1)) ↦ α : α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α))
have h : ∀ (x : α × ((i : Fin n) → α)) (x_1 : Fin (n + 1)),
  Eq (α := α)
    (((insertNthOrderIso.{u_2} (fun (x : Fin (n + 1)) ↦ α) (last n) :
            α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α)) :
          (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
        x x_1 :
      α)
    (((snocOrderIso.{u_2} (n := n) fun (x : Fin (n + 1)) ↦ α : α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α)) :
          (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
        x x_1 :
      α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Fin.Tuple (goal)
Goal:
n : ℕ
x : { x : Fin (n + 1) // x ≠ last n }
⊢ ((finSuccAboveOrderIso (last n)).symm : (a : { x : Fin (n + 1) // x ≠ last n }) → Fin n) x =
    (↑x : Fin (n + 1)).castLT ⋯
have rw : some (((finSuccAboveOrderIso (last n)).symm : (a : { x : Fin (n + 1) // x ≠ last n }) → Fin n) x) =
  some ((↑x : Fin (n + 1)).castLT sorry)
Tactic: rw [← Option.some_inj]
-- Lean 4 proof step from Mathlib.Order.Fin.Tuple (goal)
Goal:
n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x : Fin (n + 1) // x ≠ p }
⊢ ((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x =
    (p.castLT ⋯).predAbove (↑x : Fin (n + 1))
have rw : some (((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x) =
  some ((p.castLT sorry).predAbove (↑x : Fin (n + 1)))
Tactic: rw [← Option.some_inj]
-- Lean 4 proof step from Mathlib.Order.FixedPoints (hypothesis)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
⊢ p ((lfp : (a : α →o α) → α) f)
have hSup₁ : p (sSup s)
Tactic: specialize hSup s fun a => And.right
Cleared hypotheses: hSup