awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i : Fin (x₁.len + 1)
i_1 : Fin (x₂.len + 1)
h : (↑(Fin.castAdd (x₂.len + 1) i) : ℕ) ≤ (↑(Fin.natAdd (x₁.len + 1) i_1) : ℕ)
left :
  (↑((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) : ℕ) ≤
    y₁.len + 1 + (↑((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i_1) : ℕ)
⊢ (↑((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
            (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
                (fun (i : Fin (x₁.len + 1)) ↦
                  Fin.castAdd (y₂.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
                (fun (i : Fin (x₂.len + 1)) ↦
                  Fin.natAdd (y₁.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.castAdd (x₂.len + 1) i)) :
      ℕ) ≤
    (↑((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
            (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
                (fun (i : Fin (x₁.len + 1)) ↦
                  Fin.castAdd (y₂.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
                (fun (i : Fin (x₂.len + 1)) ↦
                  Fin.natAdd (y₁.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.natAdd (x₁.len + 1) i_1)) :
      ℕ)

Tactic:
simp at h ⊢
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i : Fin (x₂.len + 1)
i_1 : Fin (x₁.len + 1)
h : (↑(Fin.natAdd (x₁.len + 1) i) : ℕ) ≤ (↑(Fin.castAdd (x₂.len + 1) i_1) : ℕ)
right :
  y₁.len + 1 + (↑((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i) : ℕ) ≤
    (↑((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i_1) : ℕ)
⊢ (↑((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
            (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
                (fun (i : Fin (x₁.len + 1)) ↦
                  Fin.castAdd (y₂.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
                (fun (i : Fin (x₂.len + 1)) ↦
                  Fin.natAdd (y₁.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.natAdd (x₁.len + 1) i)) :
      ℕ) ≤
    (↑((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
            (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
                (fun (i : Fin (x₁.len + 1)) ↦
                  Fin.castAdd (y₂.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
                (fun (i : Fin (x₂.len + 1)) ↦
                  Fin.natAdd (y₁.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.castAdd (x₂.len + 1) i_1)) :
      ℕ)

Tactic:
simp at h ⊢
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i i_1 : Fin (x₂.len + 1)
h : (↑(Fin.natAdd (x₁.len + 1) i) : ℕ) ≤ (↑(Fin.natAdd (x₁.len + 1) i_1) : ℕ)
right :
  ∀ (h : i ≤ i_1),
    LE.le (α := Fin (y₂.len + 1))
      ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i : Fin (y₂.len + 1))
      ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i_1 : Fin (y₂.len + 1))
⊢ (↑((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
            (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
                (fun (i : Fin (x₁.len + 1)) ↦
                  Fin.castAdd (y₂.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
                (fun (i : Fin (x₂.len + 1)) ↦
                  Fin.natAdd (y₁.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.natAdd (x₁.len + 1) i)) :
      ℕ) ≤
    (↑((fun (i : Fin (x₁.len + 1 + (x₂.len + 1))) ↦
            (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
                (fun (i : Fin (x₁.len + 1)) ↦
                  Fin.castAdd (y₂.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
                (fun (i : Fin (x₂.len + 1)) ↦
                  Fin.natAdd (y₁.len + 1)
                    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.natAdd (x₁.len + 1) i_1)) :
      ℕ)

Tactic:
simp at h ⊢
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i i_1 : Fin (x₁.len + 1)
h : i ≤ i_1
⊢ LE.le (α := Fin (y₁.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i : Fin (y₁.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i_1 : Fin (y₁.len + 1))

Tactic:
grind only [OrderHom.apply_mono]

Premises used: OrderHom.apply_mono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i : Fin (x₁.len + 1)
i_1 : Fin (x₂.len + 1)
h : (↑i : ℕ) ≤ x₁.len + 1 + (↑i_1 : ℕ)
⊢ (↑((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) : ℕ) ≤
    y₁.len + 1 + (↑((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i_1) : ℕ)

Tactic:
grind only [OrderHom.apply_mono]

Premises used: OrderHom.apply_mono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i : Fin (x₂.len + 1)
i_1 : Fin (x₁.len + 1)
h : x₁.len + 1 + (↑i : ℕ) ≤ (↑i_1 : ℕ)
⊢ y₁.len + 1 + (↑((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i) : ℕ) ≤
    (↑((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i_1) : ℕ)

Tactic:
grind only [OrderHom.apply_mono]

Premises used: OrderHom.apply_mono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i i_1 : Fin (x₂.len + 1)
h : i ≤ i_1
⊢ LE.le (α := Fin (y₂.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i : Fin (y₂.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i_1 : Fin (y₂.len + 1))

Tactic:
grind only [OrderHom.apply_mono]

Premises used: OrderHom.apply_mono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ (tensorObjOf x y).len + z.len + 1 = x.len + (tensorObjOf y z).len + 1

Tactic:
simp +arith
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y₁ y₂ : AugmentedSimplexCategory
f : y₁ ⟶ y₂
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y₁ ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y₂)
    (𝟙 x ⊗ₘ f) (x ◁ f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁ x₂ y : AugmentedSimplexCategory
f : x₁ ⟶ x₂
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x₁ y ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x₂ y)
    (f ⊗ₘ 𝟙 y) (f ▷ y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x : AugmentedSimplexCategory
of :
  ∀ (a : SimplexCategory),
    WithInitial.of a ◁ 𝟙 WithInitial.star =
      𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of a) WithInitial.star)
star :
  Eq (α :=
    Quiver.Hom (V := AugmentedSimplexCategory)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
    (WithInitial.star ◁ 𝟙 WithInitial.star)
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
⊢ x ◁ 𝟙 WithInitial.star = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x WithInitial.star)

Tactic:
cases x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
a : SimplexCategory
⊢ WithInitial.of a ◁ 𝟙 WithInitial.star =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of a) WithInitial.star)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
⊢ Eq (α :=
    Quiver.Hom (V := AugmentedSimplexCategory)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
    (WithInitial.star ◁ 𝟙 WithInitial.star)
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x : AugmentedSimplexCategory
of :
  ∀ (a : SimplexCategory),
    𝟙 WithInitial.star ▷ WithInitial.of a =
      𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of a))
star :
  Eq (α :=
    Quiver.Hom (V := WithInitial SimplexCategory)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
    (𝟙 WithInitial.star ▷ WithInitial.star)
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
⊢ 𝟙 WithInitial.star ▷ x = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star x)

Tactic:
cases x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
a : SimplexCategory
⊢ 𝟙 WithInitial.star ▷ WithInitial.of a =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of a))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
⊢ Eq (α :=
    Quiver.Hom (V := WithInitial SimplexCategory)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
    (𝟙 WithInitial.star ▷ WithInitial.star)
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : SimplexCategory
i : Fin (x.len + 1)
dsimp :
  Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom
            (𝟙 (WithInitial.of x) ≫
              𝟙 (WithInitial.of x) ≫
                SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.castAddOrderEmb (y.len + 1))) ≫ eqToHom ⋯) :
          (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1))
        i :
      Fin (x.len + y.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1) + 1))
⊢ Eq (α := Fin ((tensorObjOf x y).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x y) : (a : Fin (x.len + 1)) → Fin ((tensorObjOf x y).len + 1)) i :
      Fin ((tensorObjOf x y).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1)).succ)

Tactic:
dsimp [inl', inl, MonoidalCategoryStruct.rightUnitor, MonoidalCategoryStruct.whiskerLeft,
    tensorHom, WithInitial.down, rightUnitor, tensorObj]

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, AugmentedSimplexCategory.rightUnitor, AugmentedSimplexCategory.tensorObj, CategoryTheory.MonoidalCategoryStruct.rightUnitor, AugmentedSimplexCategory.tensorHom, CategoryTheory.WithInitial.down, AugmentedSimplexCategory.inl', AugmentedSimplexCategory.inl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : SimplexCategory
i : Fin (x.len + 1)
h :
  (↑((SimplexCategory.Hom.toOrderHom
              (𝟙 (WithInitial.of x) ≫
                𝟙 (WithInitial.of x) ≫
                  SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.castAddOrderEmb (y.len + 1))) ≫ eqToHom ⋯) :
            (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1))
          i) :
      ℕ) =
    (↑(Fin.cast ⋯ (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1) + 1)) : ℕ)
⊢ Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom
            (𝟙 (WithInitial.of x) ≫
              𝟙 (WithInitial.of x) ≫
                SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.castAddOrderEmb (y.len + 1))) ≫ eqToHom ⋯) :
          (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1))
        i :
      Fin (x.len + y.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1) + 1))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : SimplexCategory
i : Fin (x.len + 1)
⊢ (↑((SimplexCategory.Hom.toOrderHom
              (𝟙 (WithInitial.of x) ≫
                𝟙 (WithInitial.of x) ≫
                  SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.castAddOrderEmb (y.len + 1))) ≫ eqToHom ⋯) :
            (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1))
          i) :
      ℕ) =
    (↑(Fin.cast ⋯ (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1) + 1)) : ℕ)

Tactic:
simp [OrderEmbedding.toOrderHom]

Premises used: OrderEmbedding.toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : SimplexCategory
i : Fin (y.len + 1)
dsimp :
  Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom
            (𝟙 (WithInitial.of y) ≫
              𝟙 (WithInitial.of y) ≫
                SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.natAddOrderEmb (x.len + 1))) ≫ eqToHom ⋯) :
          (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1))
        i :
      Fin (x.len + y.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i) : Fin (x.len + (y.len + 1) + 1))
⊢ Eq (α := Fin ((tensorObjOf x y).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf x y).len + 1)) i :
      Fin ((tensorObjOf x y).len + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ i) : Fin (x.len + (y.len + 1)).succ)

Tactic:
dsimp [inr', inr, MonoidalCategoryStruct.leftUnitor, MonoidalCategoryStruct.whiskerRight,
    tensorHom, WithInitial.down, leftUnitor, tensorObj]

Premises used: AugmentedSimplexCategory.inr', AugmentedSimplexCategory.tensorObj, CategoryTheory.MonoidalCategoryStruct.leftUnitor, AugmentedSimplexCategory.leftUnitor, CategoryTheory.MonoidalCategoryStruct.whiskerRight, AugmentedSimplexCategory.tensorHom, CategoryTheory.WithInitial.down, AugmentedSimplexCategory.inr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : SimplexCategory
i : Fin (y.len + 1)
h :
  (↑((SimplexCategory.Hom.toOrderHom
              (𝟙 (WithInitial.of y) ≫
                𝟙 (WithInitial.of y) ≫
                  SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.natAddOrderEmb (x.len + 1))) ≫ eqToHom ⋯) :
            (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1))
          i) :
      ℕ) =
    (↑(Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) : ℕ)
⊢ Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom
            (𝟙 (WithInitial.of y) ≫
              𝟙 (WithInitial.of y) ≫
                SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.natAddOrderEmb (x.len + 1))) ≫ eqToHom ⋯) :
          (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1))
        i :
      Fin (x.len + y.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i) : Fin (x.len + (y.len + 1) + 1))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : SimplexCategory
i : Fin (y.len + 1)
⊢ (↑((SimplexCategory.Hom.toOrderHom
              (𝟙 (WithInitial.of y) ≫
                𝟙 (WithInitial.of y) ≫
                  SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.natAddOrderEmb (x.len + 1))) ≫ eqToHom ⋯) :
            (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1))
          i) :
      ℕ) =
    (↑(Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) : ℕ)

Tactic:
simp [OrderEmbedding.toOrderHom]

Premises used: OrderEmbedding.toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y) ⟶
    WithInitial.of z
h₁ : inl (WithInitial.of x) (WithInitial.of y) ≫ f = inl (WithInitial.of x) (WithInitial.of y) ≫ g
h₂ : inr (WithInitial.of x) (WithInitial.of y) ≫ f = inr (WithInitial.of x) (WithInitial.of y) ≫ g
change :
  ∀ (f g : tensorObjOf x y ⟶ z)
    (h₁ :
      Eq (α := WithInitial.of x ⟶ WithInitial.of z)
        (CategoryStruct.comp (Y :=
          MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
          (inl (WithInitial.of x) (WithInitial.of y)) f)
        (CategoryStruct.comp (Y :=
          MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
          (inl (WithInitial.of x) (WithInitial.of y)) g))
    (h₂ :
      Eq (α := WithInitial.of y ⟶ WithInitial.of z)
        (CategoryStruct.comp (Y :=
          MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
          (inr (WithInitial.of x) (WithInitial.of y)) f)
        (CategoryStruct.comp (Y :=
          MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
          (inr (WithInitial.of x) (WithInitial.of y)) g)),
    f = g
⊢ f = g

Tactic:
change (tensorObjOf x y) ⟶ z at f g

Premises used: AugmentedSimplexCategory.tensorObjOf
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ :
  Eq (α := WithInitial.of x ⟶ WithInitial.of z)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inl (WithInitial.of x) (WithInitial.of y)) f)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inl (WithInitial.of x) (WithInitial.of y)) g)
h₂ :
  Eq (α := WithInitial.of y ⟶ WithInitial.of z)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inr (WithInitial.of x) (WithInitial.of y)) f)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inr (WithInitial.of x) (WithInitial.of y)) g)
⊢ inl' x y ≫ f = inl' x y ≫ g

Tactic:
change inl' _ _ ≫ f = inl' _ _ ≫ g at h₁

Premises used: AugmentedSimplexCategory.inl'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₂ :
  Eq (α := WithInitial.of y ⟶ WithInitial.of z)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inr (WithInitial.of x) (WithInitial.of y)) f)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inr (WithInitial.of x) (WithInitial.of y)) g)
h₁ : inl' x y ≫ f = inl' x y ≫ g
⊢ inr' x y ≫ f = inr' x y ≫ g

Tactic:
change inr' _ _ ≫ f = inr' _ _ ≫ g at h₂

Premises used: AugmentedSimplexCategory.inr'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
h :
  ∀ (i : Fin ((tensorObjOf x y).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)) f :
              (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
            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)) g :
              (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
            i) :
        ℕ)
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
⊢ i = Fin.cast ⋯ j

Tactic:
have : i = j.cast (Nat.succ_add x.len (y.len + 1)) := rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j
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)) f :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast ⋯ 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)) g :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast ⋯ 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)) f :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          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)) g :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          i) :
      ℕ)

Tactic:
rw [this]