awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : ¬y = i
⊢ i.succ ≤ y.castSucc
have neg : ∀ (h' : (↑i : ℕ) ≤ (↑y : ℕ)) (h'' : ¬(↑y : ℕ) = (↑i : ℕ)), (↑i : ℕ) + 1 ≤ (↑y : ℕ)
Tactic: simp only [Fin.lt_def, Fin.le_iff_val_le_val, Fin.val_succ, Fin.val_castSucc,
        Nat.lt_succ_iff, Fin.ext_iff] at h' h'' ⊢
Cleared hypotheses: h', h''
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
⊢ ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'
have hθ₁ : ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
    ¬x = x_1
Tactic: simp only [Function.Injective, exists_prop, not_forall] at hθ
Cleared hypotheses: hθ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y
have rcases : ∀ (x y : Fin (n + 1 + 1))
  (h₁ :
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)))
  (h₂ : ¬x = y),
  ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y
Tactic: rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
Cleared hypotheses: hθ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : ¬x = y
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y
have pos : ∀ (h : x < y),
  ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y
Tactic: by_cases h : x < y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : ¬x = y
pos :
  ∀ (h : x < y),
    ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
      Eq (α := Fin (Δ'.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
        x < y
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y
have neg : ∀ (h : ¬x < y),
  ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y
Tactic: by_cases h : x < y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : ¬x = y
h : ¬x < y
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y
have neg : y < x
Tactic: refine ⟨y, x, ⟨h₁.symm, ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
⊢ ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'
have hθ₂ : ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
    x < y
Tactic: have hθ₂ : ∃ x y : Fin (n + 2), (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y := by
    rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
    by_cases h : x < y
    · exact ⟨x, y, ⟨h₁, h⟩⟩
    · refine ⟨y, x, ⟨h₁.symm, ?_⟩⟩
      lia
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
hθ₂ :
  ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y
⊢ ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'
have rcases : ∀ (x y : Fin (n + 2))
  (h₁ :
    Eq (α := Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)))
  (h₂ : x < y), ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'
Tactic: rcases hθ₂ with ⟨x, y, ⟨h₁, h₂⟩⟩
Cleared hypotheses: hθ₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
x y : Fin (n + 2)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : x < y
⊢ ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'
have h : ∃ (θ' : ⦋n⦌ ⟶ Δ'), θ = σ (x.castPred sorry) ≫ θ'
Tactic: use x.castPred ((Fin.le_last _).trans_lt' h₂).ne
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
x y : Fin (n + 2)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : x < y
⊢ ∃ (θ' : ⦋n⦌ ⟶ Δ'), θ = σ (x.castPred ⋯) ≫ θ'
have h : Eq (α := Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred sorry).castSucc : Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred sorry).succ : Fin (Δ'.len + 1))
Tactic: apply eq_σ_comp_of_not_injective'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
x y : Fin (n + 2)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : x < y
⊢ Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
have h : LE.le (α := Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred sorry).castSucc : Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred sorry).succ : Fin (Δ'.len + 1))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
x y : Fin (n + 2)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : x < y
h :
  LE.le (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
have h₃ : LE.le (α := Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred sorry).succ : Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred sorry).castSucc : Fin (Δ'.len + 1))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
x y : Fin (n + 2)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : x < y
⊢ LE.le (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).castSucc : Fin (Δ'.len + 1))
have h : LE.le (α := Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred sorry).succ : Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
Tactic: rw [Fin.castSucc_castPred, h₁]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
⊢ ∃ (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i
have h : θ = (θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i
Tactic: use θ ≫ σ (.predAbove (.last n) i)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
⊢ θ = (θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i
have h : ∀ (x : Fin (Δ.len + 1)),
  Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom ((θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x :
      Fin (⦋n + 1⦌.len + 1))
Tactic: ext x : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
x : Fin (Δ.len + 1)
this : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom ((θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x :
      Fin (⦋n + 1⦌.len + 1))
have dsimp : (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (n + 1 + 1)) x =
  i.succAbove (((Fin.last n).predAbove i).predAbove ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (n + 1 + 1)) x))
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
x : Fin (Δ.len + 1)
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom ((θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x :
      Fin (⦋n + 1⦌.len + 1))
have h : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
Tactic: suffices ∀ j ≠ i, i.succAbove (((Fin.last n).predAbove i).predAbove j) = j by
    dsimp [δ, σ]
    exact .symm <| this _ (hi _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
x : Fin (Δ.len + 1)
j : Fin (n + 2)
hj : j ≠ i
⊢ i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
have h : ∀
  (hi :
    ∀ (x : Fin (Δ.len + 1)),
      Ne (α := Fin (⦋n + 1⦌.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
        (Fin.last (n + 1) : Fin (n + 1 + 1)))
  (hj : j ≠ Fin.last (n + 1)),
  Fin.succAbove (Fin.last (n + 1)) (((Fin.last n).predAbove (Fin.last (n + 1))).predAbove j) = j
Tactic: cases i using Fin.lastCases
Cleared hypotheses: i, hi, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
x : Fin (Δ.len + 1)
j : Fin (n + 2)
hj : j ≠ i
h :
  ∀
    (hi :
      ∀ (x : Fin (Δ.len + 1)),
        Ne (α := Fin (⦋n + 1⦌.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
          (Fin.last (n + 1) : Fin (n + 1 + 1)))
    (hj : j ≠ Fin.last (n + 1)),
    Fin.succAbove (Fin.last (n + 1)) (((Fin.last n).predAbove (Fin.last (n + 1))).predAbove j) = j
⊢ i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
have h₁ : ∀ (i : Fin (n + 1))
  (hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i.castSucc)
  (hj : j ≠ i.castSucc), i.castSucc.succAbove (((Fin.last n).predAbove i.castSucc).predAbove j) = j
Tactic: cases i using Fin.lastCases
Cleared hypotheses: i, hi, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ :
  ¬Function.Surjective (α := Fin (Δ.len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1))
⊢ ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i
have obtain : ∀ (i : Fin (⦋n + 1⦌.len + 1))
  (hi : ¬∃ (a : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) a = i),
  ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i
Tactic: obtain ⟨i, hi⟩ := not_forall.mp hθ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ :
  ¬Function.Surjective (α := Fin (Δ.len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1))
i : Fin (⦋n + 1⦌.len + 1)
hi : ¬∃ (a : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) a = i
⊢ ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i
have h : ∃ (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i
Tactic: use i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
⊢ ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (⦋n⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
have rw : ¬Mono θ
Tactic: rw [← mono_iff_injective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
⊢ ∃ (i : Fin (n + 1)), θ = σ i
have obtain : ∀ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ ⦋n⦌) (h : θ = σ i ≫ θ'), ∃ (i : Fin (n + 1)), θ = σ i
Tactic: obtain ⟨i, θ', h⟩ := eq_σ_comp_of_not_injective θ (by
    rw [← mono_iff_injective]
    grind [→ le_of_mono])
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ ∃ (i : Fin (n + 1)), θ = σ i
have h₁ : θ = σ i
Tactic: use i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ θ = σ i
have this : Epi (σ i ≫ θ')
Tactic: haveI : Epi (σ i ≫ θ') := by
    rw [← h]
    infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this : Epi (σ i ≫ θ')
⊢ θ = σ i
have this₁ : Epi θ'
Tactic: haveI := CategoryTheory.epi_of_epi (σ i) θ'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this_1 : Epi (σ i ≫ θ')
this : Epi θ'
⊢ θ = σ i
have h₁ : σ i ≫ θ' = σ i
Tactic: rw [h, eq_id_of_epi θ', Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this_1 : Epi (σ i ≫ θ')
this : Epi θ'
h₁ : σ i ≫ θ' = σ i
⊢ θ = σ i
have h₂ : σ i ≫ 𝟙 ⦋n⦌ = σ i
Tactic: rw [h, eq_id_of_epi θ', Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this_1 : Epi (σ i ≫ θ')
this : Epi θ'
h₁ : σ i ≫ θ' = σ i
h₂ : σ i ≫ 𝟙 ⦋n⦌ = σ i
⊢ θ = σ i
have h₃ : σ i = σ i
Tactic: rw [h, eq_id_of_epi θ', Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
⊢ ¬Function.Surjective (α := Fin (⦋n⦌.len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
have rw : ¬Epi θ
Tactic: rw [← epi_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
⊢ ∃ (i : Fin (n + 2)), θ = δ i
have obtain : ∀ (i : Fin (n + 2)) (θ' : ⦋n⦌ ⟶ ⦋n⦌) (h : θ = θ' ≫ δ i), ∃ (i : Fin (n + 2)), θ = δ i
Tactic: obtain ⟨i, θ', h⟩ := eq_comp_δ_of_not_surjective θ (by
    rw [← epi_iff_surjective]
    grind [→ le_of_epi])
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ ∃ (i : Fin (n + 2)), θ = δ i
have h₁ : θ = δ i
Tactic: use i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ θ = δ i
have this : Mono (θ' ≫ δ i)
Tactic: haveI : Mono (θ' ≫ δ i) := by
    rw [← h]
    infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this : Mono (θ' ≫ δ i)
⊢ θ = δ i
have this₁ : Mono θ'
Tactic: haveI := CategoryTheory.mono_of_mono θ' (δ i)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this_1 : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ θ = δ i
have h₁ : θ' ≫ δ i = δ i
Tactic: rw [h, eq_id_of_mono θ', Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this_1 : Mono (θ' ≫ δ i)
this : Mono θ'
h₁ : θ' ≫ δ i = δ i
⊢ θ = δ i
have h₂ : 𝟙 ⦋n⦌ ≫ δ i = δ i
Tactic: rw [h, eq_id_of_mono θ', Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this_1 : Mono (θ' ≫ δ i)
this : Mono θ'
h₁ : θ' ≫ δ i = δ i
h₂ : 𝟙 ⦋n⦌ ≫ δ i = δ i
⊢ θ = δ i
have h₃ : δ i = δ i
Tactic: rw [h, eq_id_of_mono θ', Category.id_comp]