-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
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)
⊢ 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 (inr' 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 (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))
have a : Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
  ((SimplexCategory.Hom.toOrderHom (eqToHom sorry) : (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 sorry) :
            (a : Fin (x₁.len + x₂.len + 1 + 1)) → Fin (x₁.len + 1 + x₂.len + 1))
          (Fin.cast sorry (Fin.natAdd x₁.len.succ i)))) :
    Fin (y₁.len + y₂.len + 1 + 1))
  (Fin.cast sorry
      (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: rw [e₁, e₂]