-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
w :
  ∀ (y : Y.HomotopyCategory) (z : Z.HomotopyCategory),
    Eq (α :=
      (((Functor.obj Functor.curry₃
                      (Equivalence.inverse
                          (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x₀)).obj
              y).obj
          z ⟶
        (((Functor.obj Functor.curry₃
                      (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                        inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                  (mk x₁)).obj
              y).obj
          z)
      (NatTrans.app
        (NatTrans.app
          ((Functor.obj Functor.curry₃
                  (Equivalence.inverse (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
                    (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                      inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙ mapHomotopyCategory (Iso.hom (α_ X Y Z)))).map
              (homMk e) ≫
            Iso.hom
              ((fun
                    (x :
                      X.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  (mkNatIso
                      (fun
                          (y :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))) ↦
                        mkNatIso
                          (fun
                              (z :
                                Z.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            Iso.refl
                              ((((Functor.obj Functor.curry₃
                                            (Equivalence.inverse
                                                (prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                                  Z.HomotopyCategory) ⋙
                                              (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                                inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                                                  mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                                        (mk x)).obj
                                    (mk y)).obj
                                (mk z)))
                          ⋯)
                      ⋯ :
                    (Functor.obj Functor.curry₃
                            (Equivalence.inverse
                                (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
                              (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                                  mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                        (mk x) ≅
                      (Functor.obj Functor.curry₃
                            (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                              inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                        (mk x)))
                x₁))
          y)
        z)
      (NatTrans.app
        (NatTrans.app
          (Iso.hom
              ((fun
                    (x :
                      X.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  (mkNatIso
                      (fun
                          (y :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))) ↦
                        mkNatIso
                          (fun
                              (z :
                                Z.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            Iso.refl
                              ((((Functor.obj Functor.curry₃
                                            (Equivalence.inverse
                                                (prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                                  Z.HomotopyCategory) ⋙
                                              (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                                inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                                                  mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                                        (mk x)).obj
                                    (mk y)).obj
                                (mk z)))
                          ⋯)
                      ⋯ :
                    (Functor.obj Functor.curry₃
                            (Equivalence.inverse
                                (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
                              (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                                  mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                        (mk x) ≅
                      (Functor.obj Functor.curry₃
                            (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                              inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                        (mk x)))
                x₀) ≫
            (Functor.obj Functor.curry₃
                  (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                    inverse X (tensorObj (𝒞 := Functor.category) Y Z))).map
              (homMk e))
          y)
        z)
⊢ (Functor.obj Functor.curry₃
            (Equivalence.inverse (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
              (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙ mapHomotopyCategory (Iso.hom (α_ X Y Z)))).map
        (homMk e) ≫
      Iso.hom
        ((fun
              (x :
                X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (mkNatIso
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  mkNatIso
                    (fun
                        (z :
                          Z.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      Iso.refl
                        ((((Functor.obj Functor.curry₃
                                      (Equivalence.inverse
                                          (prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                            Z.HomotopyCategory) ⋙
                                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                                  (mk x)).obj
                              (mk y)).obj
                          (mk z)))
                    ⋯)
                ⋯ :
              (Functor.obj Functor.curry₃
                      (Equivalence.inverse
                          (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x) ≅
                (Functor.obj Functor.curry₃
                      (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                        inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                  (mk x)))
          x₁) =
    Iso.hom
        ((fun
              (x :
                X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (mkNatIso
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  mkNatIso
                    (fun
                        (z :
                          Z.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      Iso.refl
                        ((((Functor.obj Functor.curry₃
                                      (Equivalence.inverse
                                          (prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                            Z.HomotopyCategory) ⋙
                                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                                  (mk x)).obj
                              (mk y)).obj
                          (mk z)))
                    ⋯)
                ⋯ :
              (Functor.obj Functor.curry₃
                      (Equivalence.inverse
                          (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x) ≅
                (Functor.obj Functor.curry₃
                      (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                        inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                  (mk x)))
          x₀) ≫
      (Functor.obj Functor.curry₃
            (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙ inverse X (tensorObj (𝒞 := Functor.category) Y Z))).map
        (homMk e)

Tactic:
ext y z