awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : SimplexCategoryᵒᵖ
⊢ (ed.s' ≫ X.left.map (Quiver.Hom.op (SimplexCategory.isTerminalZero.from (unop n)))) ≫ X.hom.app n = 𝟙 X.right
have rw : ed.s' ≫ X.hom.app (op ⦋0⦌) = 𝟙 X.right
Tactic: rw [assoc, dsimp% X.hom.naturality, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
⊢ ed.s' ≫ X.left.σ₀Iter n ⋯ = ed.section_.app (op ⦋n⦌)
have dsimp : ed.s' ≫ X.left.map (SimplexCategory.σ₀Iter n sorry).op =
  ed.s' ≫ X.left.map (Quiver.Hom.op (SimplexCategory.isTerminalZero.from ⦋n⦌))
Tactic: dsimp [section_, SimplicialObject.σ₀Iter]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
⊢ ed.s' ≫ X.left.map (SimplexCategory.σ₀Iter n ⋯).op =
    ed.s' ≫ X.left.map (Quiver.Hom.op (SimplexCategory.isTerminalZero.from ⦋n⦌))
have e_a : SimplexCategory.σ₀Iter n sorry = SimplexCategory.isTerminalZero.from ⦋n⦌
Tactic: congr 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
j : ℕ
hj : j = (↑i.rev : ℕ)
⊢ h ed i = X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s j ≫ X.left.σ₀Iter (↑i : ℕ) ⋯
have subst : h ed i = X.left.δ₀Iter (↑i : ℕ) sorry ≫ ed.s (↑i.rev : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) sorry
Tactic: subst hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
⊢ h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = (X.hom ≫ ed.section_).app (op ⦋n⦌)
have dsimp : h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
⊢ h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)
have rw : X.hom.app (op ⦋n⦌) ≫ ed.s' ≫ X.left.σ₀Iter (↑(Fin.last n) : ℕ) sorry = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)
Tactic: rw [h_eq_assoc _ _ 0, X.left.σ₀Iter_δ' _ _ 1 (by grind),
      ed.s₀_comp_δ₁_assoc, X.δ₀Iter_hom_app_assoc _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
⊢ h ed j.succ ≫ X.left.δ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
have generalize : ∀ (k : Fin (n + 1 + 1)) (hk : j.succ.rev = k),
  h ed j.succ ≫ X.left.δ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
Tactic: generalize hk : j.succ.rev = k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ h ed j.succ ≫ X.left.δ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
have dsimp : h ed j.succ ≫ X.left.δ i.castSucc = X.left.δ i ≫ h ed j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ h ed j.succ ≫ X.left.δ i.castSucc = X.left.δ i ≫ h ed j
have rw : X.left.δ₀Iter (↑j.succ : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.succ : ℕ) sorry ≫ X.left.δ i.castSucc =
  X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry
Tactic: rw [h_eq_assoc _ _ k, h_eq _ _ k]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ X.left.δ₀Iter (↑j.succ : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.succ : ℕ) ⋯ ≫ X.left.δ i.castSucc =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯
have dsimp : X.left.δ₀Iter ((↑j : ℕ) + 1) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) sorry ≫ X.left.δ i.castSucc =
  X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯
have rw : X.left.δ₀Iter ((↑j : ℕ) + 1) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry =
  X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry
Tactic: rw [X.left.σ₀Iter_δ _ _ (by grind), X.left.δ_δ₀Iter_assoc _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
rw :
  X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯
⊢ X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯
have rw₁ : X.left.δ₀Iter ((↑j : ℕ) + 1) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry =
  X.left.δ₀Iter ((↑j : ℕ) + 1) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry
Tactic: rw [X.left.σ₀Iter_δ _ _ (by grind), X.left.δ_δ₀Iter_assoc _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ
have generalize : ∀ (k : Fin (n + 1 + 1)) (hk : i.succ.rev = k),
  h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ
Tactic: generalize hk : i.succ.rev = k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ
have dsimp : h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ
have rw : X.left.δ₀Iter (↑i.succ : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i.succ : ℕ) sorry ≫ X.left.δ i.castSucc.succ =
  X.left.δ₀Iter (↑i.castSucc : ℕ) sorry ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i.castSucc : ℕ) sorry ≫ X.left.δ i.castSucc.succ
Tactic: rw [h_eq_assoc _ _ k, h_eq_assoc _ _ (k + 1)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ X.left.δ₀Iter (↑i.succ : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i.succ : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i.castSucc : ℕ) ⋯ ≫
      ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i.castSucc : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
have dsimp : X.left.δ₀Iter ((↑i : ℕ) + 1) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) sorry ≫ X.left.δ i.castSucc.succ =
  X.left.δ₀Iter (↑i : ℕ) sorry ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) sorry ≫ X.left.δ i.castSucc.succ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ X.left.δ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
have rw : X.left.δ₀Iter (↑i : ℕ) sorry ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) sorry ≫ X.left.δ i.castSucc.succ =
  X.left.δ₀Iter (↑i : ℕ) sorry ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) sorry ≫ X.left.δ i.castSucc.succ
Tactic: rw [X.left.δ₀Iter_succ'_assoc _ (by grind),
      X.left.σ₀Iter_δ' i.castSucc.succ i.val (m := k.val + 1)
        (i' := 1) (by grind) (by grind) (by simp; grind),
      dsimp% ed.s_comp_δ_assoc k.val 0, X.left.σ₀Iter_δ _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
rw :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
⊢ X.left.δ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
have rw₁ : X.left.δ₀Iter (↑i : ℕ) sorry ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) sorry ≫ X.left.δ i.castSucc.succ =
  X.left.δ₀Iter (↑i : ℕ) sorry ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.δ 1 ≫ X.left.σ₀Iter (↑i : ℕ) sorry
Tactic: rw [X.left.δ₀Iter_succ'_assoc _ (by grind),
      X.left.σ₀Iter_δ' i.castSucc.succ i.val (m := k.val + 1)
        (i' := 1) (by grind) (by grind) (by simp; grind),
      dsimp% ed.s_comp_δ_assoc k.val 0, X.left.σ₀Iter_δ _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
rw :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
rw₁ :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.δ 1 ≫ X.left.σ₀Iter (↑i : ℕ) ⋯
⊢ X.left.δ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
have rw₂ : X.left.δ₀Iter (↑i : ℕ) sorry ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) sorry ≫ X.left.δ i.castSucc.succ =
  X.left.δ₀Iter (↑i : ℕ) sorry ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) sorry
Tactic: rw [X.left.δ₀Iter_succ'_assoc _ (by grind),
      X.left.σ₀Iter_δ' i.castSucc.succ i.val (m := k.val + 1)
        (i' := 1) (by grind) (by grind) (by simp; grind),
      dsimp% ed.s_comp_δ_assoc k.val 0, X.left.σ₀Iter_δ _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
rw :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
rw₁ :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.δ 1 ≫ X.left.σ₀Iter (↑i : ℕ) ⋯
rw₂ :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯
⊢ X.left.δ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
have rw₃ : X.left.δ₀Iter (↑i : ℕ) sorry ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) sorry =
  X.left.δ₀Iter (↑i : ℕ) sorry ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) sorry
Tactic: rw [X.left.δ₀Iter_succ'_assoc _ (by grind),
      X.left.σ₀Iter_δ' i.castSucc.succ i.val (m := k.val + 1)
        (i' := 1) (by grind) (by grind) (by simp; grind),
      dsimp% ed.s_comp_δ_assoc k.val 0, X.left.σ₀Iter_δ _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
⊢ h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
have generalize : ∀ (k : Fin (n + 1)) (hk : j.rev = k),
  h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
Tactic: generalize hk : j.rev = k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
⊢ ∃ (l : ℕ), (↑i : ℕ) = (↑j : ℕ) + 1 + l
have rw : ∀ (hij : (↑j.succ : ℕ) ≤ (↑i : ℕ)) (k : Fin (n + 1)) (hk : j.rev = k), ∃ (l : ℕ), (↑i : ℕ) = (↑j : ℕ) + 1 + l
Tactic: rw [Fin.castSucc_lt_iff_succ_le, Fin.le_def] at hij
Cleared hypotheses: hij, k, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : (↑j.succ : ℕ) ≤ (↑i : ℕ)
k : Fin (n + 1)
hk : j.rev = k
⊢ ∃ (l : ℕ), (↑i : ℕ) = (↑j : ℕ) + 1 + l
have obtain : ∀ (l : ℕ) (hl : (↑j.succ : ℕ) + l = (↑i : ℕ)), ∃ (l : ℕ), (↑i : ℕ) = (↑j : ℕ) + 1 + l
Tactic: obtain ⟨l, hl⟩ := Nat.le.dest hij
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
⊢ h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
have obtain : ∀ (l : ℕ) (hl : (↑i : ℕ) = (↑j : ℕ) + 1 + l),
  h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
Tactic: obtain ⟨l, hl⟩ : ∃ l, i.val = j + 1 + l := by
      rw [Fin.castSucc_lt_iff_succ_le, Fin.le_def] at hij
      obtain ⟨l, hl⟩ := Nat.le.dest hij
      exact ⟨l, by grind⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : (↑i : ℕ) = (↑j : ℕ) + 1 + l
⊢ h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
have this : ed.s ((↑k : ℕ) + 1) ≫ X.left.δ (⟨l + 1, sorry⟩ : Fin ((↑k : ℕ) + 2)).succ =
  X.left.δ (⟨l + 1, sorry⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)
Tactic: have := ed.s_comp_δ k ⟨l + 1, by grind⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : (↑i : ℕ) = (↑j : ℕ) + 1 + l
this :
  ed.s ((↑k : ℕ) + 1) ≫ X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)).succ =
    X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)
⊢ h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
have dsimp : h ed j.castSucc ≫ X.left.δ i.succ = X.left.δ i ≫ h ed j
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : (↑i : ℕ) = (↑j : ℕ) + 1 + l
this :
  ed.s ((↑k : ℕ) + 1) ≫ X.left.δ (⟨l + 1 + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2 + 1)) =
    X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)
⊢ h ed j.castSucc ≫ X.left.δ i.succ = X.left.δ i ≫ h ed j
have rw : X.left.δ i ≫ X.left.δ₀Iter (↑j.castSucc : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.castSucc : ℕ) sorry =
  X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry
Tactic: rw [h_eq_assoc _ _ (k + 1), h_eq _ _ k,
      X.left.σ₀Iter_δ' _ _ ⟨l + 2, by grind⟩ (by grind),
      reassoc_of% this, ← X.left.δ_δ₀Iter'_assoc _ _ i (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ h ed j ≫ X.left.σ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.succ
have generalize : ∀ (k : Fin (n + 1)) (hk : j.rev = k),
  h ed j ≫ X.left.σ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.succ
Tactic: generalize hk : j.rev = k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ h ed j ≫ X.left.σ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.succ
have dsimp : h ed j ≫ X.left.σ i.castSucc = X.left.σ i ≫ h ed j.succ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ h ed j ≫ X.left.σ i.castSucc = X.left.σ i ≫ h ed j.succ
have rw : X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry ≫ X.left.σ i.castSucc =
  X.left.σ i ≫ X.left.δ₀Iter (↑j.succ : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.succ : ℕ) sorry
Tactic: rw [h_eq_assoc _ _ k, h_eq _ _ k]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ ≫ X.left.σ i.castSucc =
    X.left.σ i ≫ X.left.δ₀Iter (↑j.succ : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.succ : ℕ) ⋯
have dsimp : X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry ≫ X.left.σ i.castSucc =
  X.left.σ i ≫ X.left.δ₀Iter ((↑j : ℕ) + 1) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ ≫ X.left.σ i.castSucc =
    X.left.σ i ≫ X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯
have rw : X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) sorry ≫ X.left.σ i.castSucc =
  X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) sorry
Tactic: rw [X.left.σ_δ₀Iter_assoc _ _ (by grind), X.left.σ₀Iter_σ _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
rw :
  X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ ≫ X.left.σ i.castSucc =
    X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯
⊢ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ ≫ X.left.σ i.castSucc =
    X.left.σ i ≫ X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯
have rw₁ : X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) sorry =
  X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) sorry
Tactic: rw [X.left.σ_δ₀Iter_assoc _ _ (by grind), X.left.σ₀Iter_σ _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
⊢ h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc
have generalize : ∀ (k : Fin (n + 1)) (hk : j.rev = k),
  h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc
Tactic: generalize hk : j.rev = k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
⊢ h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc
have obtain : ∀ (l : ℕ) (hl : (↑j : ℕ) + l = (↑i : ℕ)),
  h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc
Tactic: obtain ⟨l, hl⟩ := Nat.le.dest (Fin.le_def.1 hij)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : (↑j : ℕ) + l = (↑i : ℕ)
⊢ h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc
have dsimp : h ed j ≫ X.left.σ i.succ = X.left.σ i ≫ h ed j.castSucc
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : (↑j : ℕ) + l = (↑i : ℕ)
⊢ h ed j ≫ X.left.σ i.succ = X.left.σ i ≫ h ed j.castSucc
have rw : X.left.δ₀Iter (↑j : ℕ) sorry ≫ ed.s (↑k : ℕ) ≫ X.left.σ (⟨l + 1, sorry⟩ : Fin ((↑k : ℕ) + 1 + 1)) ≫ X.left.σ₀Iter (↑j : ℕ) sorry =
  X.left.δ₀Iter (↑j.castSucc : ℕ) sorry ≫
    ed.s (↑k : ℕ) ≫ X.left.σ (⟨l, sorry⟩ : Fin ((↑k : ℕ) + 1)).succ ≫ X.left.σ₀Iter (↑j.castSucc : ℕ) sorry
Tactic: rw [h_eq_assoc _ _ k, h_eq _ _ (k + 1),
      X.left.σ_δ₀Iter'_assoc _ _ ⟨l, by grind⟩
        (by grind),
      ← ed.s_comp_σ_assoc,
      X.left.σ₀Iter_σ' j i.succ ⟨l + 1, by grind⟩ (by grind)]