awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : (↑i : ℕ) ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : (↑k : ℕ) < j
neg :
  (↑((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 (j + 1) ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (m + 1))
          (i.succAbove k)) :
      ℕ) =
    0
⊢ (↑((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 (j + 1) ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (m + 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)) (δ i) :
              (a : Fin (n + 1)) → Fin (n + 1 + 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 j ⋯) :
            (a : Fin (n + 1)) → Fin (m + 1))
          k) :
      ℕ)

Tactic:
rw [σ₀Iter_coe_eq_of_lt j .., coe_δ]

Premises used: SimplexCategory.coe_δ, SimplexCategory.σ₀Iter_coe_eq_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : (↑i : ℕ) ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : (↑k : ℕ) < j
pos :
  ∀ (hk' : i ≤ k.castSucc),
    (↑((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 (j + 1) ⋯) :
              (a : Fin (n + 1 + 1)) → Fin (m + 1))
            (i.succAbove k)) :
        ℕ) =
      0
neg :
  ∀ (hk' : k.castSucc < i),
    (↑((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 (j + 1) ⋯) :
              (a : Fin (n + 1 + 1)) → Fin (m + 1))
            (i.succAbove k)) :
        ℕ) =
      0
⊢ (↑((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 (j + 1) ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (m + 1))
          (i.succAbove k)) :
      ℕ) =
    0

Tactic:
by_cases! hk' : i ≤ k.castSucc

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : (↑i : ℕ) ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : (↑k : ℕ) < j
hk' : i ≤ k.castSucc
pos :
  (↑((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 (j + 1) ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (m + 1))
          k.succ) :
      ℕ) =
    0
pos₁ pos₂ : Eq (α := ℕ) 0 0
⊢ (↑((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 (j + 1) ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (m + 1))
          (i.succAbove k)) :
      ℕ) =
    0

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ hk', σ₀Iter_coe_eq_of_lt ..]

Premises used: Fin.succAbove_of_le_castSucc, SimplexCategory.σ₀Iter_coe_eq_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : (↑i : ℕ) ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : (↑k : ℕ) < j
hk' : k.castSucc < i
⊢ k.castSucc < i

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : (↑i : ℕ) ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : (↑k : ℕ) < j
hk' : k.castSucc < i
neg :
  (↑((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 (j + 1) ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (m + 1))
          k.castSucc) :
      ℕ) =
    0
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ (↑((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 (j + 1) ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (m + 1))
          (i.succAbove k)) :
      ℕ) =
    0

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (by lia), σ₀Iter_coe_eq_of_lt ..]

Premises used: SimplexCategory.σ₀Iter_coe_eq_of_lt, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + 0 = n
hi' : 0 < (↑i : ℕ)
hi'' : (↑i : ℕ) = (↑i' : ℕ) + 0
⊢ n = m

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + 0 = n
hi' : 0 < (↑i : ℕ)
hi'' : (↑i : ℕ) = (↑i' : ℕ) + 0
zero : ∀ (i' : Fin (n + 2)) (h : n + 0 = n) (hi'' : (↑i : ℕ) = (↑i' : ℕ) + 0), δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i'
⊢ δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i'

Tactic:
obtain rfl : n = m := by lia

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
hi' : 0 < (↑i : ℕ)
i' : Fin (n + 2)
h : n + 0 = n
hi'' : (↑i : ℕ) = (↑i' : ℕ) + 0
⊢ i = i'

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
hi' : 0 < (↑i : ℕ)
i' : Fin (n + 2)
h : n + 0 = n
hi'' : (↑i : ℕ) = (↑i' : ℕ) + 0
zero : ∀ (hi'' : (↑i : ℕ) = (↑i : ℕ) + 0), δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i
⊢ δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i'

Tactic:
obtain rfl : i = i' := by lia

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
hi' : 0 < (↑i : ℕ)
h : n + 0 = n
hi'' : (↑i : ℕ) = (↑i : ℕ) + 0
⊢ δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n) (hi' : j < (↑i : ℕ))
    (hi'' : (↑i : ℕ) = (↑i' : ℕ) + j), δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < (↑i : ℕ)
hi'' : (↑i : ℕ) = (↑i' : ℕ) + (j + 1)
⊢ m + 1 + j = n

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n) (hi' : j < (↑i : ℕ))
    (hi'' : (↑i : ℕ) = (↑i' : ℕ) + j), δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < (↑i : ℕ)
hi'' : (↑i : ℕ) = (↑i' : ℕ) + (j + 1)
⊢ j < (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n) (hi' : j < (↑i : ℕ))
    (hi'' : (↑i : ℕ) = (↑i' : ℕ) + j), δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < (↑i : ℕ)
hi'' : (↑i : ℕ) = (↑i' : ℕ) + (j + 1)
⊢ (↑i : ℕ) = (↑i'.succ : ℕ) + j

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n) (hi' : j < (↑i : ℕ))
    (hi'' : (↑i : ℕ) = (↑i' : ℕ) + j), δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < (↑i : ℕ)
hi'' : (↑i : ℕ) = (↑i' : ℕ) + (j + 1)
⊢ 0 < (↑i' : ℕ)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n) (hi' : j < (↑i : ℕ))
    (hi'' : (↑i : ℕ) = (↑i' : ℕ) + j), δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < (↑i : ℕ)
hi'' : (↑i : ℕ) = (↑i' : ℕ) + (j + 1)
succ : δ i ≫ σ₀Iter j ⋯ ≫ σ 0 = σ₀Iter (j + 1) ⋯ ≫ δ i'
succ₁ : δ i ≫ σ₀Iter j ⋯ ≫ σ 0 = σ₀Iter j ⋯ ≫ σ 0 ≫ δ i'
succ₂ : σ₀Iter j ⋯ ≫ δ i'.succ ≫ σ 0 = σ₀Iter j ⋯ ≫ σ 0 ≫ δ i'
succ₃ succ₄ : σ₀Iter j ⋯ ≫ σ 0 ≫ δ i' = σ₀Iter j ⋯ ≫ σ 0 ≫ δ i'
⊢ δ i ≫ σ₀Iter (j + 1) ⋯ = σ₀Iter (j + 1) ⋯ ≫ δ i'

Tactic:
rw [σ₀Iter_succ _, σ₀Iter_succ_assoc _,
      reassoc_of% hj _ i'.succ (by lia) (by lia) (by grind),
      dsimp% δ_comp_σ_of_gt (i := i') (j := 0)
        (by rw [Fin.lt_def]; dsimp; lia)]

Premises used: Fin.succ, SimplexCategory.σ₀Iter_succ, SimplexCategory.δ_comp_σ_of_gt, SimplexCategory.σ₀Iter_succ_assoc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : m + j = n
hi' : j < (↑i : ℕ)
hi'' : (↑i : ℕ) = (↑i' : ℕ) + j
zero :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + 0 = n) (hi' : 0 < (↑i : ℕ))
    (hi'' : (↑i : ℕ) = (↑i' : ℕ) + 0), δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i'
succ :
  ∀ (j : ℕ)
    (hj :
      ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n) (hi' : j < (↑i : ℕ))
        (hi'' : (↑i : ℕ) = (↑i' : ℕ) + j), δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i')
    {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + (j + 1) = n) (hi' : j + 1 < (↑i : ℕ))
    (hi'' : (↑i : ℕ) = (↑i' : ℕ) + (j + 1)), δ i ≫ σ₀Iter (j + 1) ⋯ = σ₀Iter (j + 1) ⋯ ≫ δ i'
⊢ δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'

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 _, σ₀Iter_succ_assoc _,
      reassoc_of% hj _ i'.succ (by lia) (by lia) (by grind),
      dsimp% δ_comp_σ_of_gt (i := i') (j := 0)
        (by rw [Fin.lt_def]; dsimp; lia)]

Premises used: SimplexCategory.σ₀Iter_succ, SimplexCategory.δ_comp_σ_of_gt, SimplexCategory.σ₀Iter_succ_assoc, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
⊢ σ j ≫ σ₀Iter i hi = σ₀Iter (i + 1) ⋯

Tactic:
ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
refine :
  ∀ (k : Fin (⦋m + 1⦌.len + 1)),
    Eq (α := 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)) (σ j ≫ σ₀Iter i hi) :
            (a : Fin (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          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) ⋯) :
            (a : Fin (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k :
        Fin (⦋n⦌.len + 1))
⊢ σ j ≫ σ₀Iter i hi = σ₀Iter (i + 1) ⋯

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
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)) (σ j ≫ σ₀Iter i hi) :
            (a : Fin (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.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 (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ)
⊢ Eq (α := 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)) (σ j ≫ σ₀Iter i hi) :
          (a : Fin (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        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) ⋯) :
          (a : Fin (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        k :
      Fin (⦋n⦌.len + 1))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
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 ⋯) :
            (a : Fin (m + 1)) → Fin (n + 1))
          (j.predAbove 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 (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.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)) (σ j ≫ σ₀Iter i hi) :
            (a : Fin (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.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 (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ)

Tactic:
rw [dsimp% ConcreteCategory.comp_apply (σ j) (σ₀Iter i), coe_σ]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, SimplexCategory.σ₀Iter, SimplexCategory.σ, SimplexCategory.coe_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
pos :
  ∀ (hk : i < (↑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 (m + 1)) → Fin (n + 1))
            (j.predAbove 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 (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
            k) :
        ℕ)
neg :
  ∀ (hk : (↑k : ℕ) ≤ i),
    (↑((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 (m + 1)) → Fin (n + 1))
            (j.predAbove 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 (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.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 (m + 1)) → Fin (n + 1))
          (j.predAbove 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 (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ)

Tactic:
by_cases! hk : i < k.val

Premises used: Fin.val
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < (↑k : ℕ)
⊢ j.castSucc < k

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < (↑k : ℕ)
pos : (↑(k.pred ⋯) : ℕ) - i = (↑k : ℕ) - (i + 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 (m + 1)) → Fin (n + 1))
          (j.predAbove 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 (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ)

Tactic:
rw [σ₀Iter_coe_eq_of_ge (i + 1) ..,
      Fin.predAbove_of_castSucc_lt _ _ (by grind),
      σ₀Iter_coe_eq_of_ge ..]

Premises used: Fin.predAbove_of_castSucc_lt, HAdd.hAdd, SimplexCategory.σ₀Iter_coe_eq_of_ge, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < (↑k : ℕ)
⊢ (↑(k.pred ⋯) : ℕ) - i = (↑k : ℕ) - (i + 1)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : (↑k : ℕ) ≤ i
neg :
  (↑((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 (m + 1)) → Fin (n + 1))
          (j.predAbove k)) :
      ℕ) =
    0
⊢ (↑((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 (m + 1)) → Fin (n + 1))
          (j.predAbove 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 (⦋m + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ)

Tactic:
rw [σ₀Iter_coe_eq_of_lt (i + 1) ..]

Premises used: SimplexCategory.σ₀Iter_coe_eq_of_lt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : (↑k : ℕ) ≤ i
rw : (↑(j.predAbove k) : ℕ) ≤ i
⊢ (↑((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 (m + 1)) → Fin (n + 1))
          (j.predAbove k)) :
      ℕ) =
    0

Tactic:
rw [σ₀Iter_coe_eq_of_le _ _ _ ?_]

Premises used: SimplexCategory.σ₀Iter_coe_eq_of_le
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : (↑k : ℕ) ≤ i
pos : ∀ (hk' : k ≤ j.castSucc), (↑(j.predAbove k) : ℕ) ≤ i
neg : ∀ (hk' : j.castSucc < k), (↑(j.predAbove k) : ℕ) ≤ i
⊢ (↑(j.predAbove k) : ℕ) ≤ i

Tactic:
by_cases! hk' : k ≤ j.castSucc

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : (↑k : ℕ) ≤ i
hk' : k ≤ j.castSucc
⊢ k ≤ j.castSucc

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : (↑k : ℕ) ≤ i
hk' : k ≤ j.castSucc
pos pos₁ pos₂ pos₃ : (↑(k.castPred ⋯) : ℕ) ≤ i
⊢ (↑(j.predAbove k) : ℕ) ≤ i

Tactic:
rwa [Fin.predAbove_of_le_castSucc _ _ (by lia)]

Premises used: Fin.predAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : (↑k : ℕ) ≤ i
hk' : j.castSucc < k
⊢ (↑(j.predAbove k) : ℕ) ≤ i

Tactic:
grind [Fin.predAbove]

Premises used: Fin.predAbove
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + 0 = m
hj : (↑j : ℕ) = (↑j' : ℕ) + 0
⊢ n = m

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + 0 = m
hj : (↑j : ℕ) = (↑j' : ℕ) + 0
zero : ∀ (j : Fin (n + 1)) (hi : n + 0 = n) (hj : (↑j : ℕ) = (↑j' : ℕ) + 0), σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j'
⊢ σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j'

Tactic:
obtain rfl : n = m := by lia

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
j' j : Fin (n + 1)
hi : n + 0 = n
hj : (↑j : ℕ) = (↑j' : ℕ) + 0
⊢ j = j'

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
j' j : Fin (n + 1)
hi : n + 0 = n
hj : (↑j : ℕ) = (↑j' : ℕ) + 0
zero : ∀ (hj : (↑j : ℕ) = (↑j : ℕ) + 0), σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j
⊢ σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j'

Tactic:
obtain rfl : j = j' := by lia

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
j : Fin (n + 1)
hi : n + 0 = n
hj : (↑j : ℕ) = (↑j : ℕ) + 0
⊢ σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
    σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ n + 1 + i = m

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
    σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ (↑j : ℕ) = (↑j'.succ : ℕ) + i

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
    σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ 0 ≤ j'

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m) (hj : (↑j : ℕ) = (↑j' : ℕ) + i),
    σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
succ : σ j ≫ σ₀Iter i ⋯ ≫ σ 0 = σ₀Iter (i + 1) ⋯ ≫ σ j'
succ₁ : σ j ≫ σ₀Iter i ⋯ ≫ σ 0 = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
succ₂ : σ₀Iter i ⋯ ≫ σ j'.succ ≫ σ 0 = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
succ₃ : σ₀Iter i ⋯ ≫ σ (Fin.castSucc 0) ≫ σ j' = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
succ₄ succ₅ : σ₀Iter i ⋯ ≫ σ 0 ≫ σ j' = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
⊢ σ j ≫ σ₀Iter (i + 1) hi = σ₀Iter (i + 1) ⋯ ≫ σ j'

Tactic:
rw [σ₀Iter_succ, σ₀Iter_succ_assoc,
      reassoc_of% hi' _ j'.succ (by lia) (by grind),
      ← σ_comp_σ (by simp), Fin.castSucc_zero]

Premises used: Fin.succ, SimplexCategory.σ₀Iter_succ, Fin.castSucc_zero, SimplexCategory.σ₀Iter_succ_assoc, SimplexCategory.σ_comp_σ