awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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.ι φ) = φ
rw₃ rw₄ : φ = φ
⊢ factorThruImage φ = e

Tactic:
rw [← cancel_mono i, fac, ← image_ι_eq fac, image.fac]

Premises used: SimplexCategory.image_ι_eq, CategoryTheory.Limits.image.fac, CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
⊢ toPartOrd.obj n = { carrier := ULift.{u, 0} (Fin (n.len + 1)), str := ULift.instPartialOrder }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
i : Fin (n.len + 1)
⊢ Eq (α := ULift.{u, 0} (Fin (m.len + 1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrd.{u}) ↦ (↑x1 : Type u) →o (↑x2 : Type u)) (CC := PartOrd.carrier)
            (toPartOrd.map f) :
          (a : ULift.{u, 0} (Fin (n.len + 1))) → ULift.{u, 0} (Fin (m.len + 1)))
        { down := i :
          ULift.{u, 0}
            (↑(Functor.obj
                  (forget₂ FinPartOrd (FC := fun (x1 x2 : FinPartOrd.{0}) ↦
                    (↑x1.toPartOrd : Type) →o (↑x2.toPartOrd : Type)) (CC := fun (X : FinPartOrd.{0}) ↦
                    (↑X.toPartOrd : Type)) PartOrd (FD := fun (x1 x2 : PartOrd.{0}) ↦ (↑x1 : Type) →o (↑x2 : Type))
                    (CD := PartOrd.carrier))
                  (Functor.obj
                    (forget₂ NonemptyFinLinOrd (FC := fun (x1 x2 : NonemptyFinLinOrd.{0}) ↦
                      (↑x1.toLinOrd : Type) →o (↑x2.toLinOrd : Type)) (CC := fun (X : NonemptyFinLinOrd.{0}) ↦
                      (↑X.toLinOrd : Type)) FinPartOrd (FD := fun (x1 x2 : FinPartOrd.{0}) ↦
                      (↑x1.toPartOrd : Type) →o (↑x2.toPartOrd : Type)) (CD := fun (X : FinPartOrd.{0}) ↦
                      (↑X.toPartOrd : Type)))
                    (NonemptyFinLinOrd.of (Fin (n.len + 1))))) :
              Type) } :
      ULift.{u, 0} (Fin (m.len + 1)))
    ({
        down :=
          (ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
              (a : Fin (n.len + 1)) → Fin (m.len + 1))
            i } :
      ULift.{u, 0} (Fin (m.len + 1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
⊢ (↑(toCat.obj ⦋n⦌) : Type) = Fin (n + 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ HasTerminal SimplexCategory

Tactic:
IsTerminal.hasTerminal isTerminalZero

Premises used: SimplexCategory.isTerminalZero, CategoryTheory.Limits.IsTerminal.hasTerminal
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
rw : i.succAbove = j.succAbove
⊢ i = j

Tactic:
rw [← Fin.succAbove_left_inj]

Premises used: Fin.succAbove_left_inj
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
h : ∀ (k : Fin (n + 1)), i.succAbove k = j.succAbove k
⊢ i.succAbove = j.succAbove

Tactic:
ext k : 1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
k : Fin (n + 1)
⊢ i.succAbove k = j.succAbove k

Tactic:
congr($hij k)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
k : Fin (n + 1)
⊢ i.succAbove k = j.succAbove k

Tactic:
exact congr($hij k)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
rw : i.predAbove = j.predAbove
⊢ i = j

Tactic:
rw [← Fin.predAbove_left_inj]

Premises used: Fin.predAbove_left_inj
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
h : ∀ (k : Fin (n + 1 + 1)), i.predAbove k = j.predAbove k
⊢ i.predAbove = j.predAbove

Tactic:
ext k : 1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
k : Fin (n + 1 + 1)
⊢ i.predAbove k = j.predAbove k

Tactic:
congr($hij k)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
k : Fin (n + 1 + 1)
⊢ i.predAbove k = j.predAbove k

Tactic:
exact congr($hij k)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
n : ℕ
⊢ ⦋n⦌.len = n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
n : SimplexCategory
⊢ ⦋n.len⦌ = n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
a b : SimplexCategory
f g : a.Hom b
⊢ f.toOrderHom = g.toOrderHom → f = g

Tactic:
id

Premises used: SimplexCategory.Hom, id, SimplexCategory.Hom.toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
a b : SimplexCategory
f : a.Hom b
⊢ mk f.toOrderHom = f

Tactic:
rfl

Premises used: SimplexCategory.Hom.toOrderHom, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
a b : SimplexCategory
f : Fin (a.len + 1) →o Fin (b.len + 1)
⊢ (mk f).toOrderHom = f

Tactic:
rfl

Premises used: SimplexCategory.Hom.toOrderHom, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
a b : SimplexCategory
f : Fin (a.len + 1) →o Fin (b.len + 1)
i : Fin (a.len + 1)
⊢ Eq (α := Fin (b.len + 1)) (((mk f).toOrderHom : (a : Fin (a.len + 1)) → Fin (b.len + 1)) i : Fin (b.len + 1))
    ((f : (a : Fin (a.len + 1)) → Fin (b.len + 1)) i : Fin (b.len + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
a : SimplexCategory
⊢ Hom.toOrderHom (𝟙 a) = OrderHom.id

Tactic:
rfl

Premises used: OrderHom.id, SimplexCategory.Hom.id, SimplexCategory.Hom.toOrderHom, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
a b c : SimplexCategory
f : a ⟶ b
g : b ⟶ c
⊢ Hom.toOrderHom (f ≫ g) = (Hom.toOrderHom g).comp (Hom.toOrderHom f)

Tactic:
rfl

Premises used: OrderHom.comp, SimplexCategory.Hom.comp, SimplexCategory.Hom.toOrderHom, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
a b : SimplexCategory
f g : a ⟶ b
⊢ toOrderHom f = toOrderHom g → f = g

Tactic:
Hom.ext' _ _

Premises used: SimplexCategory.Hom.ext'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
n : ℕ
⊢ ⦋0⦌.len ≤ n

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
n : ℕ
a b : Truncated n
f g : a ⟶ b
h : Hom.toOrderHom f.hom = Hom.toOrderHom g.hom
⊢ f = g

Tactic:
ObjectProperty.hom_ext _ (SimplexCategory.Hom.ext _ _ h)

Premises used: SimplexCategory.Hom.ext, CategoryTheory.ObjectProperty.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
n : ℕ
a : SimplexCategory
ha : a.len ≤ n
⊢ tr (𝟙 a) ha ha = 𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) a ha)

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
n : ℕ
a b c : SimplexCategory
f : a ⟶ b
g : b ⟶ c
ha : a.len ≤ n
hb : b.len ≤ n
hc : c.len ≤ n
⊢ tr (f ≫ g) ha hc = tr f ha hb ≫ tr g hb hc

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Defs
Goal:
n : ℕ
a b c : SimplexCategory
f : a ⟶ b
hb : b.len ≤ n
hc : c.len ≤ n
g :
  Quiver.Hom (V := ObjectProperty.FullSubcategory (C := SimplexCategory) fun (a : SimplexCategory) ↦ a.len ≤ n)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) b hb)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) c hc)
ha : a.len ≤ n
⊢ tr (f ≫ g.hom) ha hc = tr f ha hb ≫ g

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
hi : n + i = m
j : Fin (⦋n⦌.len + 1)
⊢ (↑j : ℕ) + i < ⦋m⦌.len + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
hi : n + i = m
x x_1 : Fin (⦋n⦌.len + 1)
⊢ x ≤ x_1 →
    LE.le (α := Fin (⦋m⦌.len + 1)) ((fun (j : Fin (⦋n⦌.len + 1)) ↦ (⟨(↑j : ℕ) + i, ⋯⟩ : Fin (⦋m⦌.len + 1))) x)
      ((fun (j : Fin (⦋n⦌.len + 1)) ↦ (⟨(↑j : ℕ) + i, ⋯⟩ : Fin (⦋m⦌.len + 1))) x_1)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (n + 1)
hi : autoParam (n + i = m) δ₀Iter_apply._auto_1
⊢ (↑j : ℕ) + i < ⦋m⦌.len + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (n + 1)
hi : n + i = m
⊢ (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) :
        (a : Fin (n + 1)) → Fin (m + 1))
      j =
    (⟨(↑j : ℕ) + i, ⋯⟩ : Fin (m + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
⊢ δ₀Iter 0 ⋯ = 𝟙 ⦋n⦌

Tactic:
rfl

Premises used: OrderHom.id, SimplexCategory.Hom.id, SimplexCategory.δ₀Iter, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
⊢ Eq (α := ⦋n⦌ ⟶ ⦋n + 1⦌) (δ₀Iter 1 ⋯) (δ 0)

Tactic:
rfl

Premises used: Fin.succAbove, Fin.succ, SimplexCategory.mkHom, SimplexCategory.δ, OrderEmbedding.toOrderHom, rfl, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + i = m
⊢ δ₀Iter (i + 1) ⋯ = δ₀Iter i h ≫ δ 0

Tactic:
rfl

Premises used: Fin.succAbove, Fin.succ, OrderHom.comp, SimplexCategory.Hom.comp, SimplexCategory.δ₀Iter, rfl, ite, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
⊢ δ₀Iter (i + 1) h = δ 0 ≫ δ₀Iter i ⋯

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

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

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

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
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 (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 ⋯) :
            (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)) (δ₀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))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
h₁ : (↑k : ℕ) + (i + 1) = (↑k : ℕ) + 1 + i
⊢ (↑(⟨(↑k : ℕ) + (i + 1), ⋯⟩ : Fin (m + 1)) : ℕ) = (↑(⟨(↑(Fin.succAbove 0 k) : ℕ) + i, ⋯⟩ : Fin (m + 1)) : ℕ)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ (↑k : ℕ) + (i + 1) = (↑k : ℕ) + 1 + i

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

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ j ≤ ⟨(↑k : ℕ) + i, ⋯⟩.castSucc

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
h : (↑(⟨(↑k : ℕ) + i, ⋯⟩ : Fin (m + 1)).succ : ℕ) = (↑(⟨(↑k : ℕ) + (i + 1), ⋯⟩ : Fin (m + 1 + 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) :
      ℕ)

Tactic:
rw [dsimp% ConcreteCategory.comp_apply (δ₀Iter i hi) (δ j), coe_δ,
    δ₀Iter_apply .., δ₀Iter_apply ..,
    Fin.succAbove_of_le_castSucc _ _ (by grind)]

Premises used: Fin.succAbove_of_le_castSucc, SimplexCategory.coe_δ, CategoryTheory.ConcreteCategory.comp_apply, SimplexCategory.δ, SimplexCategory.δ₀Iter, SimplexCategory.δ₀Iter_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ (↑(⟨(↑k : ℕ) + i, ⋯⟩ : Fin (m + 1)).succ : ℕ) = (↑(⟨(↑k : ℕ) + (i + 1), ⋯⟩ : Fin (m + 1 + 1)) : ℕ)

Tactic:
simp [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + 0 = m
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 : n + 0 = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + 0
zero : ∀ (i' : Fin (n + 2)) (h : n + 0 = n) (hi'' : (↑i' : ℕ) = (↑i : ℕ) + 0), δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯
⊢ δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯

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

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
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 i' : Fin (n + 2)
h : n + 0 = n
hi'' : (↑i' : ℕ) = (↑i : ℕ) + 0
zero : ∀ (hi'' : (↑i : ℕ) = (↑i : ℕ) + 0), δ₀Iter 0 h ≫ δ i = δ i ≫ δ₀Iter 0 ⋯
⊢ δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯

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

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

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
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)
⊢ 0 ≤ i

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
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)
⊢ (↑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 : 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'
rw : n + 1 + j = m
succ₄ : δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ 0 ≫ δ₀Iter j ⋯ ≫ δ i'
rw₁ : n + 1 + j = m
⊢ δ₀Iter (j + 1) h ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯

Tactic:
rw [δ₀Iter_succ'_assoc .., δ₀Iter_succ' ..,
      ← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),
      ← hj _ i' _ (by grind)]

Premises used: SimplexCategory.δ₀Iter_succ'_assoc, SimplexCategory.δ_comp_δ, SimplexCategory.δ₀Iter_succ'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
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 ⋯
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 ⋯)
    {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) ⋯
⊢ δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯

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)]

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

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 + 1) = m + 1
hj : (↑j : ℕ) ≤ i
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 ⋯) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
          k :
        Fin (⦋m⦌.len + 1))
⊢ δ₀Iter (i + 1) hi ≫ σ j = δ₀Iter i ⋯

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 + 1) = m + 1
hj : (↑j : ℕ) ≤ i
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 (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) :
      ℕ)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ j.castSucc < ⟨(↑k : ℕ) + (i + 1), ⋯⟩

Tactic:
grind