-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
w x y z : AugmentedSimplexCategory
h₁ :
  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))
h₂ :
  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))
h₃ :
  (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inr 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)) =
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inr 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))
⊢ (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
      Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
        (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
    Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
      Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))
have h₄ : (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
          (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inr
      z ≫
    (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
      Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
        (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
  (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
          (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inr
      z ≫
    Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
      Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))
Tactic: ext