-- 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 (inr' 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.natAdd x₁.len.succ i) : Fin (x₁.len + (x₂.len + 1)).succ)
e₂ :
  Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' 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.natAdd y₁.len.succ
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂) : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)
a :
  Eq (α := Fin (y₁.len + 1 + y₂.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))
        (Fin.natAdd (x₁.len + 1) i) :
      Fin (y₁.len + 1 + (y₂.len + 1)))
    (Fin.natAdd (y₁.len + 1)
        ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂) : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i) :
      Fin (y₁.len + 1 + (y₂.len + 1)))
⊢ 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))
            (Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)))) :
      Fin (y₁.len + y₂.len + 1 + 1))
    (Fin.cast ⋯
        (Fin.natAdd y₁.len.succ
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂) : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)

Tactic:
simp only [SimplexCategory.eqToHom_toOrderHom, SimplexCategory.len_mk,
      Nat.succ_eq_add_one, OrderEmbedding.toOrderHom_coe,
      OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply,
      Fin.cast_cast, Fin.cast_eq_self, Fin.cast_inj]

Premises used: SimplexCategory.len_mk, Nat.succ_eq_add_one, OrderEmbedding.toOrderHom_coe, OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply, SimplexCategory.eqToHom_toOrderHom, Fin.cast_cast, Fin.cast_eq_self, Fin.cast_inj