awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
change :
  inr' x y ≫
      inl' (tensorObjOf x y) z ≫
        WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))) =
    inl' y z ≫ inr' x (tensorObjOf y z)
⊢ Eq (α :=
    WithInitial.of y ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x)
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))
    (inr (WithInitial.of x) (WithInitial.of y) ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y)).inl
          (WithInitial.of z) ≫
        Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))
    (inl (WithInitial.of y) (WithInitial.of z) ≫
      inr (WithInitial.of x)
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))

Tactic:
change inr' _ _ ≫ inl' _ _ ≫ WithInitial.down _ = inl' _ _ ≫ inr' _ _

Premises used: AugmentedSimplexCategory.inr', CategoryTheory.WithInitial.down, AugmentedSimplexCategory.inl'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
a :
  ∀ (i : Fin (y.len + 1)),
    Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
      ((SimplexCategory.Hom.toOrderHom
              (inr' x y ≫
                inl' (tensorObjOf x y) z ≫
                  WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))) :
            (a : Fin (y.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
          i :
        Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
      ((SimplexCategory.Hom.toOrderHom (inl' y z ≫ inr' x (tensorObjOf y z)) :
            (a : Fin (y.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
          i :
        Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
⊢ inr' x y ≫
      inl' (tensorObjOf x y) z ≫
        WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))) =
    inl' y z ≫ inr' x (tensorObjOf y z)

Tactic:
ext i : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
a :
  Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
            (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
          ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
⊢ Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (inr' x y ≫
              inl' (tensorObjOf x y) z ≫
                WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))) :
          (a : Fin (y.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z ≫ inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))

Tactic:
dsimp [MonoidalCategoryStruct.associator, associator]

Premises used: AugmentedSimplexCategory.associator, CategoryTheory.MonoidalCategoryStruct.associator
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
⊢ Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)

Tactic:
have e₁ := inl'_eval y z i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
⊢ 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:
have e₂ := inr'_eval x y i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  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)
⊢ x.len + 1 + (y.len + 1) = (tensorObjOf x y).len + 1

Tactic:
simp +arith
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  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)
⊢ Eq (α := Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin ((tensorObjOf x y).len + 1)) → Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)) :
      Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))) :
      Fin ((tensorObjOf x y).len + (z.len + 1)).succ)

Tactic:
have e₃ := inl'_eval (tensorObjOf x y) z <| Fin.cast (by simp +arith) <| i.natAdd (x.len + 1)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  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)
e₃ :
  Eq (α := Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin ((tensorObjOf x y).len + 1)) → Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)) :
      Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))) :
      Fin ((tensorObjOf x y).len + (z.len + 1)).succ)
⊢ y.len + 1 + (z.len + 1) = (tensorObjOf y z).len + 1

Tactic:
simp +arith
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  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)
e₃ :
  Eq (α := Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin ((tensorObjOf x y).len + 1)) → Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)) :
      Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))) :
      Fin ((tensorObjOf x y).len + (z.len + 1)).succ)
⊢ Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin ((tensorObjOf y z).len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i)) :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i))) :
      Fin (x.len + ((tensorObjOf y z).len + 1)).succ)

Tactic:
have e₄ := inr'_eval x (tensorObjOf y z) <| Fin.cast (by simp +arith) <| i.castAdd (z.len + 1)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin (y.len + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i :
      Fin (y.len + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x y) : (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.succ i) : Fin (x.len + (y.len + 1)).succ)
e₃ :
  Eq (α := Fin (x.len + y.len + 1 + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)) :
      Fin (x.len + y.len + 1 + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))) :
      Fin (x.len + y.len + 1 + (z.len + 1)).succ)
e₄ :
  Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
a :
  Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)))) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
            (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
          ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))

Tactic:
rw [e₁, e₂, e₃, e₄]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin (y.len + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i :
      Fin (y.len + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x y) : (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.succ i) : Fin (x.len + (y.len + 1)).succ)
e₃ :
  Eq (α := Fin (x.len + y.len + 1 + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)) :
      Fin (x.len + y.len + 1 + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))) :
      Fin (x.len + y.len + 1 + (z.len + 1)).succ)
e₄ :
  Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
a :
  (↑((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
            (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
          (Fin.cast ⋯
            (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))))) :
      ℕ) =
    (↑(Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i)))) : ℕ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)))) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin (y.len + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i :
      Fin (y.len + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x y) : (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.succ i) : Fin (x.len + (y.len + 1)).succ)
e₃ :
  Eq (α := Fin (x.len + y.len + 1 + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)) :
      Fin (x.len + y.len + 1 + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))) :
      Fin (x.len + y.len + 1 + (z.len + 1)).succ)
e₄ :
  Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
⊢ (↑((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
            (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
          (Fin.cast ⋯
            (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))))) :
      ℕ) =
    (↑(Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i)))) : ℕ)

Tactic:
simp +arith
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y z x_1 x_2 : AugmentedSimplexCategory
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α :=
    WithInitial.star ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star x_2))
    (x_1.inr WithInitial.star ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 WithInitial.star).inl x_2 ≫
        Iso.hom (α_ x_1 WithInitial.star x_2))
    (inl WithInitial.star x_2 ≫
      x_1.inr (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star x_2))
⊢ Eq (α :=
    WithInitial.star ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star x_2))
    (x_1.inr WithInitial.star ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 WithInitial.star).inl x_2 ≫
        Iso.hom (α_ x_1 WithInitial.star x_2))
    (inl WithInitial.star x_2 ≫
      x_1.inr (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star x_2))

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : AugmentedSimplexCategory
h₁ : x.inl y ≫ (𝟙 x ⊗ₘ 𝟙 y) = x.inl y ≫ 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)
h₂ : x.inr y ≫ (𝟙 x ⊗ₘ 𝟙 y) = x.inr y ≫ 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)
⊢ 𝟙 x ⊗ₘ 𝟙 y = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : AugmentedSimplexCategory
⊢ x.inl y ≫ (𝟙 x ⊗ₘ 𝟙 y) = x.inl y ≫ 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)

Tactic:
simpa [inl, MonoidalCategoryStruct.whiskerLeft, MonoidalCategoryStruct.whiskerRight] using
      (tensorHom_comp_tensorHom (𝟙 x) (WithInitial.starInitial.to y) (𝟙 x) (𝟙 y))

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.CategoryStruct.id, CategoryTheory.WithInitial.starInitial, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.Limits.IsInitial.to, AugmentedSimplexCategory.inl, AugmentedSimplexCategory.tensorHom_comp_tensorHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : AugmentedSimplexCategory
⊢ x.inr y ≫ (𝟙 x ⊗ₘ 𝟙 y) = x.inr y ≫ 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)

Tactic:
simpa [inr, MonoidalCategoryStruct.whiskerLeft, MonoidalCategoryStruct.whiskerRight] using
      (tensorHom_comp_tensorHom (WithInitial.starInitial.to x) (𝟙 y) (𝟙 x) (𝟙 y))

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.CategoryStruct.id, CategoryTheory.WithInitial.starInitial, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.Limits.IsInitial.to, AugmentedSimplexCategory.inr, AugmentedSimplexCategory.tensorHom_comp_tensorHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
w x y z : AugmentedSimplexCategory
⊢ w.inl x ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
                (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
            z ≫
          (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
            Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
              (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
    w.inl x ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
                (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
            z ≫
          Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
            Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))

Tactic:
simp [-id_tensorHom, -tensorHom_id]

Premises used: AugmentedSimplexCategory.tensorHom_id, AugmentedSimplexCategory.id_tensorHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
w x y z : AugmentedSimplexCategory
⊢ w.inr x ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
                (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
            z ≫
          (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
            Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
              (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
    w.inr x ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
                (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
            z ≫
          Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
            Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))

Tactic:
simp [-id_tensorHom, -tensorHom_id]

Premises used: AugmentedSimplexCategory.tensorHom_id, AugmentedSimplexCategory.id_tensorHom