awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
x : SimplexCategory
e : x ≅ x
h : Finset.card (α := Fin (x.len + 1)) Finset.univ = x.len + 1
eq₁ :
  RelIso.toRelEmbedding (r := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2)
      (orderIsoOfIso e) =
    Finset.orderEmbOfFin Finset.univ h
⊢ e = Iso.refl x
have eq₂ : RelIso.toRelEmbedding (r := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2)
    (orderIsoOfIso (Iso.refl x)) =
  Finset.orderEmbOfFin Finset.univ h
Tactic: have eq₂ :=
    Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso (Iso.refl x)) i)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
x : SimplexCategory
e : x ≅ x
h : Finset.card (α := Fin (x.len + 1)) Finset.univ = x.len + 1
eq₁ :
  RelIso.toRelEmbedding (r := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2)
      (orderIsoOfIso e) =
    Finset.orderEmbOfFin Finset.univ h
eq₂ :
  RelIso.toRelEmbedding (r := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2)
      (orderIsoOfIso (Iso.refl x)) =
    Finset.orderEmbOfFin Finset.univ h
⊢ e = Iso.refl x
have w : ∀ (x_1 : Fin (x.len + 1)),
  Eq (α := Fin (x.len + 1)) ((Hom.toOrderHom e.hom : (a : Fin (x.len + 1)) → Fin (x.len + 1)) x_1 : Fin (x.len + 1))
    ((Hom.toOrderHom (Iso.hom (Iso.refl x)) : (a : Fin (x.len + 1)) → Fin (x.len + 1)) x_1 : Fin (x.len + 1))
Tactic: ext : 4
-- 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))
⊢ ∃ (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'
have h : θ = σ i ≫ δ i.succ ≫ θ
Tactic: use δ i.succ ≫ θ
-- 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))
⊢ θ = σ i ≫ δ i.succ ≫ θ
have h : ∀ (x : Fin (⦋n + 1⦌.len + 1)),
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom (σ i ≫ δ i.succ ≫ θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
Tactic: ext x : 3
-- 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)
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom (σ i ≫ δ i.succ ≫ θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
have 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))
      ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
    Fin (Δ'.len + 1))
Tactic: simp only [len_mk, σ, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
    Function.comp_apply, Fin.predAboveOrderHom_coe]
-- 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)
⊢ 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))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))
have pos : ∀ (h' : x ≤ i.castSucc),
  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))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))
Tactic: by_cases h' : x ≤ Fin.castSucc i
-- 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)
pos :
  ∀ (h' : x ≤ i.castSucc),
    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))
          ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
        Fin (Δ'.len + 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))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))
have neg : ∀ (h' : ¬x ≤ i.castSucc),
  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))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))
Tactic: by_cases h' : x ≤ Fin.castSucc i
-- 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' : x ≤ i.castSucc
⊢ 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))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))
have pos : 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))
      ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (x.castPred sorry)) :
    Fin (Δ'.len + 1))
Tactic: rw [Fin.predAbove_of_le_castSucc i x h']
-- 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' : x ≤ i.castSucc
⊢ 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))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (x.castPred ⋯)) :
      Fin (Δ'.len + 1))
have pos : 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)) (i.succ.succAbove (x.castPred sorry)) : Fin (Δ'.len + 1))
Tactic: dsimp [δ]
-- 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' : x ≤ i.castSucc
⊢ 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)) (i.succ.succAbove (x.castPred ⋯)) : Fin (Δ'.len + 1))
have pos : 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.castPred sorry).castSucc : Fin (Δ'.len + 1))
Tactic: rw [Fin.succAbove_of_castSucc_lt _ _ _]
-- 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' : x ≤ i.castSucc
pos :
  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.castPred ⋯).castSucc : Fin (Δ'.len + 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)) (i.succ.succAbove (x.castPred ⋯)) : Fin (Δ'.len + 1))
have rw : (x.castPred sorry).castSucc < i.succ
Tactic: rw [Fin.succAbove_of_castSucc_lt _ _ _]
-- 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' : x ≤ i.castSucc
⊢ 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.castPred ⋯).castSucc : Fin (Δ'.len + 1))
have pos : 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 : Fin (Δ'.len + 1))
Tactic: rw [Fin.castSucc_castPred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
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' : ¬x ≤ i.castSucc
⊢ 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))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))
have h'₁ : i.castSucc < x
Tactic: simp only [not_le] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
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' : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
⊢ 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))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))
have hy : x = y.succ
Tactic: have hy : x = y.succ := (Fin.succ_pred x _).symm
-- 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' : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
hy : x = y.succ
⊢ 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))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))
have neg : ∀ (h' : i.castSucc < y.succ) (hy : x = y.succ),
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove y.succ)) :
      Fin (Δ'.len + 1))
Tactic: rw [hy] at h' ⊢
Cleared hypotheses: hy
-- 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
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove y.succ)) :
      Fin (Δ'.len + 1))
have neg : Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
      ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
    Fin (Δ'.len + 1))
Tactic: rw [Fin.predAbove_of_castSucc_lt i y.succ h', Fin.pred_succ]
-- 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
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))
have pos : ∀ (h'' : y = i),
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))
Tactic: by_cases h'' : y = i
-- 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
pos :
  ∀ (h'' : y = i),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
          ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
        Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))
have neg : ∀ (h'' : ¬y = i),
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))
Tactic: by_cases h'' : y = i
-- 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
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))
have pos : Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
      ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i) :
    Fin (Δ'.len + 1))
Tactic: rw [h'']
-- 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
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i) :
      Fin (Δ'.len + 1))
have pos : 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 + 1)) → Fin (Δ'.len + 1))
      ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i) :
    Fin (Δ'.len + 1))
Tactic: refine hi.symm.trans ?_
-- 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
⊢ 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 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i) :
      Fin (Δ'.len + 1))
have pos : i.castSucc = (Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i
Tactic: congr 1
-- 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.castSucc = (Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i
have pos : i.castSucc = i.succ.succAbove i
Tactic: dsimp [δ]
-- 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.castSucc = i.succ.succAbove i
have pos : i.castSucc < i.succ
Tactic: rw [Fin.succAbove_of_castSucc_lt i.succ]
-- 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
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))
have neg : Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
  ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) (i.succ.succAbove y) : Fin (Δ'.len + 1))
Tactic: dsimp [δ]
-- 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
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) (i.succ.succAbove y) : Fin (Δ'.len + 1))
have neg : i.succ ≤ y.castSucc
Tactic: rw [Fin.succAbove_of_le_castSucc i.succ _]