awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
pos :
  ∀ (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 + 1) h) :
              (a : Fin (⦋m⦌.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)) (X := ⦋n + 1⦌) (σ 0) :
              (a : Fin (n + 1 + 1)) → Fin (n + 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 + 1))
              k)) :
        ℕ)
neg :
  ∀ (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 + 1) h) :
              (a : Fin (⦋m⦌.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)) (X := ⦋n + 1⦌) (σ 0) :
              (a : Fin (n + 1 + 1)) → Fin (n + 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 + 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) h) :
            (a : Fin (⦋m⦌.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)) (X := ⦋n + 1⦌) (σ 0) :
            (a : Fin (n + 1 + 1)) → Fin (n + 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 + 1))
            k)) :
      ℕ)

Tactic:
by_cases! hk : k.val ≤ i

Premises used: Fin.val
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : (↑k : ℕ) ≤ i
pos :
  0 =
    (↑(Fin.predAbove 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 + 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) h) :
            (a : Fin (⦋m⦌.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)) (X := ⦋n + 1⦌) (σ 0) :
            (a : Fin (n + 1 + 1)) → Fin (n + 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 + 1))
            k)) :
      ℕ)

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

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

Tactic:
obtain hk | rfl := hk.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk_1 : (↑k : ℕ) ≤ i
hk : (↑k : ℕ) < i
⊢ 0 =
    (↑(Fin.predAbove 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 + 1))
            k)) :
      ℕ)

Tactic:
grind [Fin.predAbove_of_le_castSucc, Fin.coe_castPred, σ₀Iter_coe_eq_of_lt]

Premises used: SimplexCategory.σ₀Iter_coe_eq_of_lt, Fin.coe_castPred, Fin.predAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
k : Fin (⦋m⦌.len + 1)
h : n + ((↑k : ℕ) + 1) = m
hk : (↑k : ℕ) ≤ (↑k : ℕ)
⊢ 0 =
    (↑(Fin.predAbove 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 (↑k : ℕ) ⋯) :
              (a : Fin (m + 1)) → Fin (n + 1 + 1))
            k)) :
      ℕ)

Tactic:
grind [Fin.predAbove_of_le_castSucc, Fin.coe_castPred, σ₀Iter_coe_eq_of_ge, tsub_self]

Premises used: tsub_self, Fin.coe_castPred, Fin.predAbove_of_le_castSucc, SimplexCategory.σ₀Iter_coe_eq_of_ge
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < (↑k : ℕ)
rw :
  LT.lt (α := Fin (n + 1 + 1)) (Fin.castSucc 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 + 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) h) :
            (a : Fin (⦋m⦌.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)) (X := ⦋n + 1⦌) (σ 0) :
            (a : Fin (n + 1 + 1)) → Fin (n + 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 + 1))
            k)) :
      ℕ)

Tactic:
rw [σ₀Iter_coe_eq_of_ge .., coe_σ,
      Fin.predAbove_of_castSucc_lt _ _ ?_, Fin.val_pred,
      σ₀Iter_coe_eq_of_ge .., Nat.sub_add_eq]

Premises used: Fin.val_pred, Fin.predAbove_of_castSucc_lt, Nat.sub_add_eq, SimplexCategory.coe_σ, SimplexCategory.σ₀Iter_coe_eq_of_ge
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < (↑k : ℕ)
rw : 0 < (↑k : ℕ) - i
⊢ LT.lt (α := Fin (n + 1 + 1)) (Fin.castSucc 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 + 1))
      k)

Tactic:
rw [Fin.lt_def, Fin.castSucc_zero, σ₀Iter_coe_eq_of_ge ..,
      Fin.coe_ofNat_eq_mod, Nat.zero_mod]

Premises used: Fin.lt_def, Fin.castSucc_zero, Fin.coe_ofNat_eq_mod, SimplexCategory.σ₀Iter_coe_eq_of_ge, Nat.zero_mod
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < (↑k : ℕ)
⊢ 0 < (↑k : ℕ) - i

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
h : n + 0 = m
⊢ n = m

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
h : n + 0 = m
zero : ∀ (h : n + 0 = n), σ₀Iter (HAdd.hAdd (α := ℕ) 0 1) ⋯ = σ 0 ≫ σ₀Iter 0 h
⊢ σ₀Iter (HAdd.hAdd (α := ℕ) 0 1) ⋯ = σ 0 ≫ σ₀Iter 0 h

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

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
h : n + 0 = n
⊢ σ₀Iter (HAdd.hAdd (α := ℕ) 0 1) ⋯ = σ 0 ≫ σ₀Iter 0 h

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

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

Tactic:
rw [σ₀Iter_succ, hi' (by lia), σ₀Iter_succ, Category.assoc]

Premises used: CategoryTheory.Category.assoc, SimplexCategory.σ₀Iter_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + i = m
zero : ∀ {n m : ℕ} (h : n + 0 = m), σ₀Iter (HAdd.hAdd (α := ℕ) 0 1) ⋯ = σ 0 ≫ σ₀Iter 0 h
succ :
  ∀ (i : ℕ) (hi' : ∀ {n m : ℕ} (h : n + i = m), σ₀Iter (i + 1) ⋯ = σ 0 ≫ σ₀Iter i h) {n m : ℕ} (h : n + (i + 1) = m),
    σ₀Iter (i + 1 + 1) ⋯ = σ 0 ≫ σ₀Iter (i + 1) h
⊢ σ₀Iter (i + 1) ⋯ = σ 0 ≫ σ₀Iter i h

Tactic:
induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    simp
  | succ i hi' =>
    rw [σ₀Iter_succ, hi' (by lia), σ₀Iter_succ, Category.assoc]

Premises used: CategoryTheory.Category.assoc, SimplexCategory.σ₀Iter_succ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : (↑i : ℕ) ≤ j + 1
⊢ δ i ≫ σ₀Iter (j + 1) h = σ₀Iter j ⋯

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

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

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

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- 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)
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)) (δ i ≫ σ₀Iter (j + 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)) (σ₀Iter j ⋯) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
          k) :
      ℕ)
⊢ 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)) (δ i ≫ σ₀Iter (j + 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)) (σ₀Iter j ⋯) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        k :
      Fin (⦋m⦌.len + 1))

Tactic:
ext
-- 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)
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 (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) :
      ℕ)
⊢ (↑((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 ≫ σ₀Iter (j + 1) h) :
            (a : Fin (n + 1)) → Fin (m + 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 [dsimp% ConcreteCategory.comp_apply (δ i) (σ₀Iter (j + 1))]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, SimplexCategory.σ₀Iter, SimplexCategory.δ, HAdd.hAdd, OfNat.ofNat
-- 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)
pos :
  ∀ (hk : j ≤ (↑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 + 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) :
        ℕ)
neg :
  ∀ (hk : (↑k : ℕ) < j),
    (↑((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) :
        ℕ)
⊢ (↑((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:
by_cases! hk : j ≤ k.val

Premises used: Fin.val
-- 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 : j ≤ (↑k : ℕ)
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))
          (i.succAbove k)) :
      ℕ) =
    (↑k : ℕ) - j
⊢ (↑((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_ge j .., coe_δ]

Premises used: SimplexCategory.coe_δ, SimplexCategory.σ₀Iter_coe_eq_of_ge
-- 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 : j ≤ (↑k : ℕ)
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)) :
        ℕ) =
      (↑k : ℕ) - j
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)) :
        ℕ) =
      (↑k : ℕ) - j
⊢ (↑((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)) :
      ℕ) =
    (↑k : ℕ) - j

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 : j ≤ (↑k : ℕ)
hk' : i ≤ k.castSucc
pos : (↑k.succ : ℕ) - (j + 1) = (↑k : ℕ) - j
⊢ (↑((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)) :
      ℕ) =
    (↑k : ℕ) - j

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

Premises used: Fin.succAbove_of_le_castSucc, SimplexCategory.σ₀Iter_coe_eq_of_ge
-- 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 : j ≤ (↑k : ℕ)
hk' : i ≤ k.castSucc
⊢ (↑k.succ : ℕ) - (j + 1) = (↑k : ℕ) - j

Tactic:
simp
-- 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 : j ≤ (↑k : ℕ)
hk' : k.castSucc < i
⊢ j = (↑k : ℕ)

Tactic:
grind [dsimp% Fin.lt_def.1 hk']

Premises used: Fin.lt_def, Iff.mp
-- 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 : j ≤ (↑k : ℕ)
hk' : k.castSucc < i
neg :
  ∀ (h : m + ((↑k : ℕ) + 1) = n + 1) (hi' : (↑i : ℕ) ≤ (↑k : ℕ) + 1) (hk : (↑k : ℕ) ≤ (↑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 ((↑k : ℕ) + 1) ⋯) :
              (a : Fin (n + 1 + 1)) → Fin (m + 1))
            (i.succAbove k)) :
        ℕ) =
      (↑k : ℕ) - (↑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 + 1) ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (m + 1))
          (i.succAbove k)) :
      ℕ) =
    (↑k : ℕ) - j

Tactic:
obtain rfl : j = k.val := by grind [dsimp% Fin.lt_def.1 hk']

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

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

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

Premises used: tsub_self, SimplexCategory.σ₀Iter_coe_eq_of_lt, Fin.succAbove_of_castSucc_lt