awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j_1
j : Fin (x.len + 1)
h :
  ∀
    (h₁ :
      Eq (α := (a : Fin (x.len + 1)) → Fin (z.len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ f)) : (a : Fin (x.len + 1)) → Fin (z.len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ g)) : (a : Fin (x.len + 1)) → Fin (z.len + 1)))
    (h₂ : inr' x y ≫ f = inr' x y ≫ g) (i : Fin ((tensorObjOf x y).len + 1)),
    let j := Fin.cast ⋯ i;
    ∀ (this : i = Fin.cast ⋯ j) (j : Fin (x.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))
              (Fin.cast ⋯ (Fin.castAdd (y.len + 1) 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 ⋯ (Fin.castAdd (y.len + 1) 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))
          (Fin.cast ⋯ (Fin.castAdd (y.len + 1) 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 ⋯ (Fin.castAdd (y.len + 1) j))) :
      ℕ)

Tactic:
rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₁

Premises used: SimplexCategory.Hom.ext_iff, OrderHom.ext_iff
-- 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 (α := (a : Fin (x.len + 1)) → Fin (z.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ f)) : (a : Fin (x.len + 1)) → Fin (z.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ g)) : (a : Fin (x.len + 1)) → Fin (z.len + 1))
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j_1 : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j_1
j : Fin (x.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))
          (Fin.cast ⋯ (Fin.castAdd (y.len + 1) 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 ⋯ (Fin.castAdd (y.len + 1) j))) :
      ℕ)

Tactic:
simpa [← inl'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₁ j

Premises used: Fin.ext_iff, CategoryTheory.ConcreteCategory.hom, congrFun, AugmentedSimplexCategory.inl'_eval
-- 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_1 : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j_1
j : Fin (y.len + 1)
h :
  ∀
    (h₂ :
      Eq (α := (a : Fin (y.len + 1)) → Fin (z.len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ f)) : (a : Fin (y.len + 1)) → Fin (z.len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ g)) : (a : Fin (y.len + 1)) → Fin (z.len + 1)))
    (i : Fin ((tensorObjOf x y).len + 1)),
    let j := Fin.cast ⋯ i;
    ∀ (this : i = Fin.cast ⋯ j) (j : Fin (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))
              (Fin.cast ⋯ (Fin.natAdd (x.len + 1) 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 ⋯ (Fin.natAdd (x.len + 1) 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))
          (Fin.cast ⋯ (Fin.natAdd (x.len + 1) 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 ⋯ (Fin.natAdd (x.len + 1) j))) :
      ℕ)

Tactic:
rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₂

Premises used: SimplexCategory.Hom.ext_iff, OrderHom.ext_iff
-- 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₂ :
  Eq (α := (a : Fin (y.len + 1)) → Fin (z.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ f)) : (a : Fin (y.len + 1)) → Fin (z.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ g)) : (a : Fin (y.len + 1)) → Fin (z.len + 1))
i : Fin ((tensorObjOf x y).len + 1)
j_1 : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j_1
j : Fin (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))
          (Fin.cast ⋯ (Fin.natAdd (x.len + 1) 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 ⋯ (Fin.natAdd (x.len + 1) j))) :
      ℕ)

Tactic:
simpa [← inr'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₂ j

Premises used: Fin.ext_iff, CategoryTheory.ConcreteCategory.hom, congrFun, AugmentedSimplexCategory.inr'_eval
-- 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 :
  ∀ (x_2 : Fin (x.len + 1 + (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))
            (Fin.cast ⋯ x_2)) :
        ℕ) =
      (↑((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 ⋯ x_2)) :
        ℕ)
⊢ (↑((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)) :
      ℕ)

Tactic:
cases j using Fin.addCases (m := x.len + 1) (n := y.len + 1) with
    | left j =>
      rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₁
      simpa [← inl'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₁ j
    | right j =>
      rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₂
      simpa [← inr'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₂ j

Premises used: Fin.ext_iff, CategoryTheory.ConcreteCategory.hom, SimplexCategory.Hom.ext_iff, OrderHom.ext_iff, congrFun, AugmentedSimplexCategory.inl'_eval, AugmentedSimplexCategory.inr'_eval
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y ⟶ z_1
x z : SimplexCategory
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) WithInitial.star ⟶
    WithInitial.of z
h₁ : inl (WithInitial.of x) WithInitial.star ≫ f = inl (WithInitial.of x) WithInitial.star ≫ g
h₂ : inr (WithInitial.of x) WithInitial.star ≫ f = inr (WithInitial.of x) WithInitial.star ≫ g
⊢ 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) WithInitial.star) ≫ f =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) WithInitial.star) ≫ g

Tactic:
simp only [inl, Category.assoc, Iso.cancel_iso_inv_left, Limits.IsInitial.to_self,
        whiskerLeft_id_star] at h₁

Premises used: CategoryTheory.Category.assoc, AugmentedSimplexCategory.whiskerLeft_id_star, CategoryTheory.Limits.IsInitial.to_self, CategoryTheory.Iso.cancel_iso_inv_left, AugmentedSimplexCategory.inl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y ⟶ z_1
x z : SimplexCategory
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) WithInitial.star ⟶
    WithInitial.of z
h₂ : inr (WithInitial.of x) WithInitial.star ≫ f = inr (WithInitial.of x) WithInitial.star ≫ g
h₁ :
  𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) WithInitial.star) ≫ f =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) WithInitial.star) ≫ g
⊢ f = g

Tactic:
simpa [Category.id_comp f, Category.id_comp g] using h₁

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y_1 ⟶ z_1
y z : SimplexCategory
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of y) ⟶
    WithInitial.of z
h₁ : inl WithInitial.star (WithInitial.of y) ≫ f = inl WithInitial.star (WithInitial.of y) ≫ g
h₂ : inr WithInitial.star (WithInitial.of y) ≫ f = inr WithInitial.star (WithInitial.of y) ≫ g
⊢ 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of y)) ≫ f =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of y)) ≫ g

Tactic:
simp only [inr, Category.assoc, Iso.cancel_iso_inv_left, Limits.IsInitial.to_self,
        id_star_whiskerRight] at h₂

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsInitial.to_self, CategoryTheory.Iso.cancel_iso_inv_left, AugmentedSimplexCategory.id_star_whiskerRight, AugmentedSimplexCategory.inr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y_1 ⟶ z_1
y z : SimplexCategory
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of y) ⟶
    WithInitial.of z
h₁ : inl WithInitial.star (WithInitial.of y) ≫ f = inl WithInitial.star (WithInitial.of y) ≫ g
h₂ :
  𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of y)) ≫ f =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of y)) ≫ g
⊢ f = g

Tactic:
simpa [Category.id_comp f, Category.id_comp g] using h₂

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
change : inl' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₁ ≫ inl' y₁ y₂
⊢ inl (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₁ ≫ inl (WithInitial.of y₁) (WithInitial.of y₂)

Tactic:
change inl' _ _ ≫ tensorHomOf _ _ = WithInitial.down f₁ ≫ inl' _ _

Premises used: AugmentedSimplexCategory.tensorHomOf, CategoryTheory.WithInitial.down, AugmentedSimplexCategory.inl'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
a :
  ∀ (i : Fin (x₁.len + 1)),
    Eq (α := Fin ((tensorObjOf y₁ y₂).len + 1))
      ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂ ≫ tensorHomOf f₁ f₂) :
            (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
          i :
        Fin ((tensorObjOf y₁ y₂).len + 1))
      ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁ ≫ inl' y₁ y₂) :
            (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
          i :
        Fin ((tensorObjOf y₁ y₂).len + 1))
⊢ inl' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₁ ≫ inl' y₁ y₂

Tactic:
ext i : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
a :
  Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯) : (a : Fin (y₁.len + 1 + y₂.len + 1)) → Fin (y₁.len + y₂.len + 1 + 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))
          ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯) :
              (a : Fin (x₁.len + x₂.len + 1 + 1)) → Fin (x₁.len + 1 + x₂.len + 1))
            ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin (x₁.len + x₂.len + 1 + 1))
              i))) :
      Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y₁ y₂) : (a : Fin (y₁.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
      Fin (y₁.len + y₂.len + 1 + 1))
⊢ Eq (α := Fin ((tensorObjOf y₁ y₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂ ≫ tensorHomOf f₁ f₂) :
          (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
        i :
      Fin ((tensorObjOf y₁ y₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁ ≫ inl' y₁ y₂) :
          (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
        i :
      Fin ((tensorObjOf y₁ y₂).len + 1))

Tactic:
dsimp [tensorHomOf]

Premises used: AugmentedSimplexCategory.tensorHomOf
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
⊢ Eq (α := Fin ((tensorObjOf x₁ x₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf x₁ x₂).len + 1)) i :
      Fin ((tensorObjOf x₁ x₂).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i) : Fin (x₁.len + (x₂.len + 1)).succ)

Tactic:
have e₁ := inl'_eval x₁ x₂ i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf x₁ x₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf x₁ x₂).len + 1)) i :
      Fin ((tensorObjOf x₁ x₂).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i) : Fin (x₁.len + (x₂.len + 1)).succ)
⊢ Eq (α := Fin ((tensorObjOf y₁ y₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y₁ y₂) : (a : Fin (y₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
        ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
      Fin ((tensorObjOf y₁ y₂).len + 1))
    (Fin.cast ⋯
        (Fin.castAdd (y₂.len + 1)
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)

Tactic:
have e₂ := inl'_eval y₁ y₂ <| (WithInitial.down f₁).toOrderHom i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
e₁ :
  Eq (α := Fin (x₁.len + x₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin (x₁.len + x₂.len + 1 + 1)) i :
      Fin (x₁.len + x₂.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i) : Fin (x₁.len + (x₂.len + 1)).succ)
e₂ :
  Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y₁ y₂) : (a : Fin (y₁.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
      Fin (y₁.len + y₂.len + 1 + 1))
    (Fin.cast ⋯
        (Fin.castAdd (y₂.len + 1)
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)
rw : Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)
| (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))
      (Fin.castAdd (x₂.len + 1) i) :
    Fin (y₁.len + 1 + (y₂.len + 1)))

Tactic:
rw [Fin.addCases_left]

Premises used: Fin.addCases_left
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
e₁ :
  Eq (α := Fin (x₁.len + x₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin (x₁.len + x₂.len + 1 + 1)) i :
      Fin (x₁.len + x₂.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i) : Fin (x₁.len + (x₂.len + 1)).succ)
e₂ :
  Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y₁ y₂) : (a : Fin (y₁.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
      Fin (y₁.len + y₂.len + 1 + 1))
    (Fin.cast ⋯
        (Fin.castAdd (y₂.len + 1)
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)
change : Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)
| (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))
      (Fin.castAdd (x₂.len + 1) i) :
    Fin (y₁.len + 1 + (y₂.len + 1)))

Tactic:
change Fin.addCases
        (fun i ↦ Fin.castAdd (y₂.len + 1) (f₁.toOrderHom i))
        (fun i ↦ Fin.natAdd (y₁.len + 1) (f₂.toOrderHom i))
        (Fin.castAdd (x₂.len + 1) i)
      rw [Fin.addCases_left]

Premises used: Fin.addCases_left