awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst : Epi e
i : Δ' ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
⊢ image φ = Δ'
have this : StrongEpi e
Tactic: haveI := strongEpi_of_epi e
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e_1 : Δ ⟶ Δ'
inst : Epi e_1
i : Δ' ⟶ Δ''
inst_1 : Mono i
fac : e_1 ≫ i = φ
this : StrongEpi e_1
e : Δ' ≅ image φ := image.isoStrongEpiMono e_1 i fac
⊢ image φ = Δ'
have len : (image φ).len = Δ'.len
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
⊢ image.ι φ = i
have this : StrongEpi e
Tactic: haveI := strongEpi_of_epi e
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image.ι φ = i
have rw : image.ι φ =
  CategoryStruct.comp (Y := image φ) (Iso.hom (image.isoStrongEpiMono e i fac) : image φ ⟶ image φ)
    (image.ι φ : image φ ⟶ Δ'')
Tactic: rw [← image.isoStrongEpiMono_hom_comp_ι e i fac,
    SimplexCategory.eq_id_of_isIso (image.isoStrongEpiMono e i fac).hom, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
this : StrongEpi e
rw :
  image.ι φ =
    CategoryStruct.comp (Y := image φ) (Iso.hom (image.isoStrongEpiMono e i fac) : image φ ⟶ image φ)
      (image.ι φ : image φ ⟶ Δ'')
⊢ image.ι φ = i
have rw₁ : image.ι φ = 𝟙 (image φ) ≫ image.ι φ
Tactic: rw [← image.isoStrongEpiMono_hom_comp_ι e i fac,
    SimplexCategory.eq_id_of_isIso (image.isoStrongEpiMono e i fac).hom, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
this : StrongEpi e
rw :
  image.ι φ =
    CategoryStruct.comp (Y := image φ) (Iso.hom (image.isoStrongEpiMono e i fac) : image φ ⟶ image φ)
      (image.ι φ : image φ ⟶ Δ'')
rw₁ : image.ι φ = 𝟙 (image φ) ≫ image.ι φ
⊢ image.ι φ = i
have rw₂ : Eq (α := image φ ⟶ Δ'') (image.ι φ) (image.ι φ)
Tactic: rw [← image.isoStrongEpiMono_hom_comp_ι e i fac,
    SimplexCategory.eq_id_of_isIso (image.isoStrongEpiMono e i fac).hom, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
⊢ factorThruImage φ = e
have rw : factorThruImage φ ≫ i = e ≫ i
Tactic: rw [← cancel_mono i, fac, ← image_ι_eq fac, image.fac]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
rw : factorThruImage φ ≫ i = e ≫ i
⊢ factorThruImage φ = e
have rw₁ : factorThruImage φ ≫ i = φ
Tactic: rw [← cancel_mono i, fac, ← image_ι_eq fac, image.fac]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
rw : factorThruImage φ ≫ i = e ≫ i
rw₁ : factorThruImage φ ≫ i = φ
⊢ factorThruImage φ = e
have rw₂ : CategoryStruct.comp (Y := image φ) (factorThruImage φ) (image.ι φ) = φ
Tactic: rw [← cancel_mono i, fac, ← image_ι_eq fac, image.fac]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
rw : factorThruImage φ ≫ i = e ≫ i
rw₁ : factorThruImage φ ≫ i = φ
rw₂ : CategoryStruct.comp (Y := image φ) (factorThruImage φ) (image.ι φ) = φ
⊢ factorThruImage φ = e
have rw₃ : φ = φ
Tactic: rw [← cancel_mono i, fac, ← image_ι_eq fac, image.fac]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
⊢ i = j
have rw : i.succAbove = j.succAbove
Tactic: rw [← Fin.succAbove_left_inj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
⊢ i.succAbove = j.succAbove
have h : ∀ (k : Fin (n + 1)), i.succAbove k = j.succAbove k
Tactic: ext k : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
⊢ i = j
have rw : i.predAbove = j.predAbove
Tactic: rw [← Fin.predAbove_left_inj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
⊢ i.predAbove = j.predAbove
have h : ∀ (k : Fin (n + 1 + 1)), i.predAbove k = j.predAbove k
Tactic: ext k : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
h : n + (i + 1) = m
⊢ δ₀Iter (i + 1) h = δ 0 ≫ δ₀Iter i ⋯
have refine : ∀ (k : Fin (⦋n⦌.len + 1)),
  Eq (α := Fin (⦋m⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) h) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k :
      Fin (⦋m⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ 0 ≫ δ₀Iter i sorry) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k :
      Fin (⦋m⦌.len + 1))
Tactic: refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ Eq (α := Fin (⦋m⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) h) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k :
      Fin (⦋m⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ 0 ≫ δ₀Iter i ⋯) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k :
      Fin (⦋m⦌.len + 1))
have h₁ : (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) h) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k) :
    ℕ) =
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ 0 ≫ δ₀Iter i sorry) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k) :
    ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ (↑(⟨(↑k : ℕ) + (i + 1), ⋯⟩ : Fin (m + 1)) : ℕ) = (↑(⟨(↑(Fin.succAbove 0 k) : ℕ) + i, ⋯⟩ : Fin (m + 1)) : ℕ)
have h₁ : (↑k : ℕ) + (i + 1) = (↑k : ℕ) + 1 + i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
⊢ δ₀Iter i hi ≫ δ j = δ₀Iter (i + 1) ⋯
have refine : ∀ (k : Fin (⦋n⦌.len + 1)),
  Eq (α := Fin (⦋m + 1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter i hi ≫ δ j) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1))
        k :
      Fin (⦋m + 1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) sorry) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1))
        k :
      Fin (⦋m + 1⦌.len + 1))
Tactic: refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ Eq (α := Fin (⦋m + 1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter i hi ≫ δ j) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1))
        k :
      Fin (⦋m + 1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) ⋯) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1))
        k :
      Fin (⦋m + 1⦌.len + 1))
have h : (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter i hi ≫ δ j) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1))
        k) :
    ℕ) =
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) sorry) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1))
        k) :
    ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter i hi ≫ δ j) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1))
          k) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) ⋯) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m + 1⦌.len + 1))
          k) :
      ℕ)
have h : (↑(⟨(↑k : ℕ) + i, sorry⟩ : Fin (m + 1)).succ : ℕ) = (↑(⟨(↑k : ℕ) + (i + 1), sorry⟩ : Fin (m + 1 + 1)) : ℕ)
Tactic: rw [dsimp% ConcreteCategory.comp_apply (δ₀Iter i hi) (δ j), coe_δ,
    δ₀Iter_apply .., δ₀Iter_apply ..,
    Fin.succAbove_of_le_castSucc _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + 0 = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + 0
⊢ δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯
have zero : ∀ (i' : Fin (n + 2)) (h : n + 0 = n) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + 0), δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 sorry
Tactic: obtain rfl : n = m := by lia
Cleared hypotheses: m, i', h, hi''
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
n : ℕ
i i' : Fin (n + 2)
h : n + 0 = n
hi'' : (↑i' : ℕ) = (↑i : ℕ) + 0
⊢ δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯
have zero : ∀ (hi'' : (↑i : ℕ) = (↑i : ℕ) + 0), δ₀Iter 0 h ≫ δ i = δ i ≫ δ₀Iter 0 sorry
Tactic: obtain rfl : i = i' := by lia
Cleared hypotheses: i', hi''
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + j),
    δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + (j + 1)
⊢ δ₀Iter (j + 1) h ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
have succ : δ 0 ≫ δ₀Iter j sorry ≫ δ i' = δ i ≫ δ₀Iter (j + 1) sorry
Tactic: rw [δ₀Iter_succ'_assoc .., δ₀Iter_succ' ..,
      ← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),
      ← hj _ i' _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + j),
    δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + (j + 1)
succ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
⊢ δ₀Iter (j + 1) h ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
have succ₁ : δ 0 ≫ δ₀Iter j sorry ≫ δ i' = δ i ≫ δ 0 ≫ δ₀Iter j sorry
Tactic: rw [δ₀Iter_succ'_assoc .., δ₀Iter_succ' ..,
      ← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),
      ← hj _ i' _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + j),
    δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + (j + 1)
succ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
succ₁ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ 0 ≫ δ₀Iter j ⋯
⊢ δ₀Iter (j + 1) h ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
have succ₂ : δ 0 ≫ δ₀Iter j sorry ≫ δ i' = δ 0 ≫ δ i.succ ≫ δ₀Iter j sorry
Tactic: rw [δ₀Iter_succ'_assoc .., δ₀Iter_succ' ..,
      ← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),
      ← hj _ i' _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + j),
    δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + (j + 1)
succ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
succ₁ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ 0 ≫ δ₀Iter j ⋯
succ₂ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ 0 ≫ δ i.succ ≫ δ₀Iter j ⋯
⊢ δ₀Iter (j + 1) h ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
have succ₃ : δ 0 ≫ δ₀Iter j sorry ≫ δ i' = δ 0 ≫ δ₀Iter j sorry ≫ δ i'
Tactic: rw [δ₀Iter_succ'_assoc .., δ₀Iter_succ' ..,
      ← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),
      ← hj _ i' _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + j),
    δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + (j + 1)
succ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
succ₁ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ 0 ≫ δ₀Iter j ⋯
succ₂ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ 0 ≫ δ i.succ ≫ δ₀Iter j ⋯
succ₃ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ 0 ≫ δ₀Iter j ⋯ ≫ δ i'
⊢ δ₀Iter (j + 1) h ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
have rw : n + 1 + j = m
Tactic: rw [δ₀Iter_succ'_assoc .., δ₀Iter_succ' ..,
      ← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),
      ← hj _ i' _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : n + j = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + j
⊢ δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
have zero : ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + 0 = m) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + 0),
  δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 sorry
Tactic: induction j generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    obtain rfl : i = i' := by lia
    simp
  | succ j hj =>
    rw [δ₀Iter_succ'_assoc .., δ₀Iter_succ' ..,
      ← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),
      ← hj _ i' _ (by grind)]
Cleared hypotheses: n, i, j, m, i', h, hi''
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : n + j = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + j
zero :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + 0 = m) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + 0),
    δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯
⊢ δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
have succ : ∀ (j : ℕ)
  (hj :
    ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + j),
      δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j sorry)
  {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + (j + 1) = m) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + (j + 1)),
  δ₀Iter (j + 1) h ≫ δ i' = δ i ≫ δ₀Iter (j + 1) sorry
Tactic: induction j generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    obtain rfl : i = i' := by lia
    simp
  | succ j hj =>
    rw [δ₀Iter_succ'_assoc .., δ₀Iter_succ' ..,
      ← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),
      ← hj _ i' _ (by grind)]
Cleared hypotheses: n, i, j, m, i', h, hi''
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
⊢ δ₀Iter (i + 1) hi ≫ σ j = δ₀Iter i ⋯
have refine : ∀ (k : Fin (⦋n⦌.len + 1)),
  Eq (α := Fin (⦋m⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) hi ≫ σ j) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k :
      Fin (⦋m⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter i sorry) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k :
      Fin (⦋m⦌.len + 1))
Tactic: refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ Eq (α := Fin (⦋m⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) hi ≫ σ j) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k :
      Fin (⦋m⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter i ⋯) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k :
      Fin (⦋m⦌.len + 1))
have h : (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) hi ≫ σ j) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k) :
    ℕ) =
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter i sorry) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k) :
    ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) hi ≫ σ j) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
          k) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter i ⋯) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
          k) :
      ℕ)
have h : (↑((⟨(↑k : ℕ) + (i + 1), sorry⟩ : Fin (m + 1 + 1)).pred sorry) : ℕ) = (↑(⟨(↑k : ℕ) + i, sorry⟩ : Fin (m + 1)) : ℕ)
Tactic: rw [dsimp% ConcreteCategory.comp_apply (δ₀Iter (i + 1)) (σ j),
    δ₀Iter_apply .., δ₀Iter_apply .., coe_σ,
    Fin.predAbove_of_castSucc_lt _ _ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + 0 = m
hj' : (↑j : ℕ) = (↑j' : ℕ) + 0
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'
have zero : ∀ (j : Fin (n + 1)) (hi' : n + 0 = n) (hj' : (↑j : ℕ) = (↑j' : ℕ) + 0), δ₀Iter 0 sorry ≫ σ j = σ j' ≫ δ₀Iter 0 hi'
Tactic: obtain rfl : n = m := by lia
Cleared hypotheses: m, j, hi', hj'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
n : ℕ
j' j : Fin (n + 1)
hi' : n + 0 = n
hj' : (↑j : ℕ) = (↑j' : ℕ) + 0
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'
have zero : ∀ (hj' : (↑j : ℕ) = (↑j : ℕ) + 0), δ₀Iter 0 sorry ≫ σ j = σ j ≫ δ₀Iter 0 hi'
Tactic: obtain rfl : j = j' := by lia
Cleared hypotheses: j', hj'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + (i + 1) = m
hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
have succ : ∀ (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi' : n + (i + 1) = 0) (hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)),
  δ₀Iter (i + 1) sorry ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
Tactic: obtain _ | m := m
Cleared hypotheses: m, j, hi', hj'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + (i + 1) = m
hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
succ :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi' : n + (i + 1) = 0) (hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)),
    δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
have succ₁ : ∀ (m : ℕ) (j : Fin (m + 1 + 1)) (hi' : n + (i + 1) = m + 1) (hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)),
  δ₀Iter (i + 1) sorry ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
Tactic: obtain _ | m := m
Cleared hypotheses: m, j, hi', hj'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
j : Fin (m + 1 + 1)
hi' : n + (i + 1) = m + 1
hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
have succ : ∀ (j : Fin (m + 1)) (hj' : (↑j.succ : ℕ) = (↑j' : ℕ) + (i + 1)), δ₀Iter (i + 1) sorry ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'
Tactic: obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero
        (by rintro rfl; dsimp at hj'; lia)
Cleared hypotheses: j, hj'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter (goal)
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : (↑j.succ : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'
have succ : δ₀Iter i sorry ≫ δ 0 ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'
Tactic: rw [δ₀Iter_succ_assoc .., δ₀Iter_succ ..,
        dsimp% δ_comp_σ_of_le (i := 0) (j := j) (by simp),
        reassoc_of% hi j j' (by lia) (by grind)]