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

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

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ :
  Eq (α := Fin (x.len + y.len + 1 + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        i :
      Fin (x.len + y.len + 1 + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i) : Fin (x.len + y.len + 1 + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin (y.len + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' y z) : (a : Fin (z.len + 1)) → Fin (y.len + z.len + 1 + 1)) i :
      Fin (y.len + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd y.len.succ i) : Fin (y.len + (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.natAdd (y.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.natAdd (y.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
⊢ (↑(Fin.cast ⋯ (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i))) : ℕ) =
    (↑(Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.natAdd (y.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) x_2 WithInitial.star))
    ((MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 x_2).inr WithInitial.star ≫
      Iso.hom (α_ x_1 x_2 WithInitial.star))
    (x_2.inr WithInitial.star ≫
      x_1.inr (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_2 WithInitial.star))
⊢ Eq (α :=
    WithInitial.star ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_2 WithInitial.star))
    ((MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 x_2).inr WithInitial.star ≫
      Iso.hom (α_ x_1 x_2 WithInitial.star))
    (x_2.inr WithInitial.star ≫
      x_1.inr (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_2 WithInitial.star))

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
change :
  Eq (α := x ⟶ tensorObjOf x (tensorObjOf y z))
    (inl' x y ≫
      inl' (tensorObjOf x y) z ≫
        WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))))
    (inl' x (tensorObjOf y z))
⊢ Eq (α :=
    WithInitial.of x ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x)
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))
    (inl (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 x)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))

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

Premises used: 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 (x.len + 1)),
    Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
      ((SimplexCategory.Hom.toOrderHom
              (inl' x y ≫
                inl' (tensorObjOf x y) z ≫
                  WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))) :
            (a : Fin (x.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
          i :
        Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
      ((SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z)) :
            (a : Fin (x.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
          i :
        Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
⊢ Eq (α := x ⟶ tensorObjOf x (tensorObjOf y z))
    (inl' x y ≫
      inl' (tensorObjOf x y) z ≫
        WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))))
    (inl' 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 (x.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 (inl' x y) : (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z)) :
          (a : Fin (x.len + 1)) → Fin (x.len + (y.len + z.len + 1) + 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
            (inl' x y ≫
              inl' (tensorObjOf x y) z ≫
                WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))) :
          (a : Fin (x.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z)) :
          (a : Fin (x.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 (x.len + 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:
have e₁ := inl'_eval x y i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ :
  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)
⊢ Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z)) :
          (a : Fin (x.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    (Fin.cast ⋯ (Fin.castAdd ((tensorObjOf y z).len + 1) i) : Fin (x.len + ((tensorObjOf y z).len + 1)).succ)

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

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

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) WithInitial.star
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 x_2))
    (inl WithInitial.star x_1 ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star x_1).inl x_2 ≫
        Iso.hom (α_ WithInitial.star x_1 x_2))
    (inl WithInitial.star (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 x_2))
⊢ Eq (α :=
    WithInitial.star ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 x_2))
    (inl WithInitial.star x_1 ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star x_1).inl x_2 ≫
        Iso.hom (α_ WithInitial.star x_1 x_2))
    (inl WithInitial.star (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 x_2))

Tactic:
cat_disch