awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
a :
  (↑(j.succAbove
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
⊢ (↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) x)) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1)) x) : ℕ)
have a₁ : (↑(j.succAbove
        ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1))))) :
    ℕ) =
  (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (↑(j.succAbove
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
have a : (↑(Fin.succ
        ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1))))) :
    ℕ) =
  (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩)) :
    ℕ)
Tactic: rw [Fin.succAbove_of_le_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
a :
  (↑(Fin.succ
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
⊢ (↑(j.succAbove
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
have a₁ : j ≤
  Fin.castSucc
    ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩))
Tactic: rw [Fin.succAbove_of_le_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (↑(j.succAbove
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)
have a : (↑(Fin.succ
        ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1))))) :
    ℕ) =
  (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩)) :
    ℕ)
Tactic: rw [Fin.succAbove_of_le_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
a :
  (↑(Fin.succ
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)
⊢ (↑(j.succAbove
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)
have a₁ : j ≤
  Fin.castSucc
    ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩))
Tactic: rw [Fin.succAbove_of_le_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ mkOfSucc i ≫ δ j = intervalEdge (↑i : ℕ) 2 ⋯
have a : ∀ (x : Fin (⦋1⦌.len + 1)),
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 sorry) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
have a : (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1)))) :
    ℕ) =
  (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 sorry) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
a :
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
have a₁ : (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1)))) :
    ℕ) =
  (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 sorry) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
have a : (↑((Hom.toOrderHom (mkOfSucc i ≫ δ i.succ.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1)))) :
    ℕ) =
  (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 sorry) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩)) :
    ℕ)
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ i.succ.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
have a : (↑i.castSucc.castSucc : ℕ) = (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 sorry) : (a : Fin 2) → Fin (n + 1 + 1)) 0) : ℕ)
Tactic: simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
      Fin.zero_eta, OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe, Function.comp_apply,
      mkOfSucc_homToOrderHom_zero, Fin.succAboveOrderEmb_apply,
      Fin.castSucc_succAbove_castSucc, Fin.succAbove_succ_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)
have a : (↑(j.succAbove i.succ) : ℕ) = (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 sorry) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)
Tactic: simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, Fin.mk_one,
      OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe, Function.comp_apply,
      mkOfSucc_homToOrderHom_one, Fin.succAboveOrderEmb_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (↑(j.succAbove i.succ) : ℕ) = (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)
have a : (↑(i.succ.castSucc.succAbove i.succ) : ℕ) =
  (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 sorry) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
⊢ (↑(i.succ.castSucc.succAbove i.succ) : ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)
have a : (↑i.succ.succ : ℕ) = (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 sorry) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)
Tactic: rw [Fin.succAbove_castSucc_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have this : LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
  ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
Tactic: have : f.toOrderHom 0 ≤ f.toOrderHom 1 := f.toOrderHom.monotone (by decide : (0 : Fin 2) ≤ 1)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have refine : f = δ 0
Tactic: refine .inl ⟨0, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
⊢ f = δ 0
have a : ∀ (i : Fin (⦋1⦌.len + 1)),
  Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
    ((Hom.toOrderHom (δ 0) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have refine : f = δ 1
Tactic: refine .inl ⟨1, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
⊢ f = δ 1
have a : ∀ (i : Fin (⦋1⦌.len + 1)),
  Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
    ((Hom.toOrderHom (δ 1) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have refine : f = δ 2
Tactic: refine .inl ⟨2, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
⊢ f = δ 2
have a : ∀ (i : Fin (⦋1⦌.len + 1)),
  Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
    ((Hom.toOrderHom (δ 2) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have refine : f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
Tactic: refine .inr ⟨f.toOrderHom 0, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
⊢ f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
have a : ∀ (i : Fin (⦋1⦌.len + 1)),
  Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
    ((Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)) :
          (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1))
        i :
      Fin (⦋2⦌.len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have refine : f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
Tactic: refine .inr ⟨f.toOrderHom 0, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
⊢ f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
have a : ∀ (i : Fin (⦋1⦌.len + 1)),
  Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
    ((Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)) :
          (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1))
        i :
      Fin (⦋2⦌.len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have refine : f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
Tactic: refine .inr ⟨f.toOrderHom 0, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
⊢ f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
have a : ∀ (i : Fin (⦋1⦌.len + 1)),
  Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
    ((Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)) :
          (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1))
        i :
      Fin (⦋2⦌.len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have this₁ : LE.le (α := Fin (⦋2⦌.len + 1)) 1 0
Tactic: rw [e0, e1] at this
Cleared hypotheses: this, e0, e1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have this₁ : LE.le (α := Fin (⦋2⦌.len + 1)) 2 0
Tactic: rw [e0, e1] at this
Cleared hypotheses: this, e0, e1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a
have this₁ : LE.le (α := Fin (⦋2⦌.len + 1)) 2 1
Tactic: rw [e0, e1] at this
Cleared hypotheses: this, e0, e1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
X Y : SimplexCategory
h : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X = Y
have len : X.len = Y.len
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
X Y : SimplexCategory
h : IsIsomorphic X Y
I : X ≅ Y
⊢ X = Y
have suffices : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
Tactic: suffices Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1)) by
    ext
    simpa
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
X Y : SimplexCategory
h : IsIsomorphic X Y
I : X ≅ Y
⊢ Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
have f : Fin (X.len + 1) ≃ Fin (Y.len + 1)
Tactic: apply Fintype.card_congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
x x_1 : SimplexCategory
f g : x ⟶ x_1
h : skeletalFunctor.map f = skeletalFunctor.map g
⊢ f = g
have a : ∀ (x_2 : Fin (x.len + 1)),
  Eq (α := Fin (x_1.len + 1)) ((Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (x_1.len + 1)) x_2 : Fin (x_1.len + 1))
    ((Hom.toOrderHom g : (a : Fin (x.len + 1)) → Fin (x_1.len + 1)) x_2 : Fin (x_1.len + 1))
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
X : NonemptyFinLinOrd
⊢ skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌ ≅ X
have aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
Tactic: have aux : Fintype.card X = Fintype.card X - 1 + 1 :=
          (Nat.succ_pred_eq_of_pos <| Fintype.card_pos_iff.mpr ⟨⊥⟩).symm