-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge y₀ y₁
w :
  ∀ (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
              (mk 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
              (mk y₁)).obj
          z)
      (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)))).obj
                (mk x)).map
            (homMk e) ≫
          Iso.hom
            ((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)).obj
                      (mk y) ≅
                    ((Functor.obj Functor.curry₃
                              (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                                inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                          (mk x)).obj
                      (mk y)))
              y₁))
        z)
      (NatTrans.app
        (Iso.hom
            ((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)).obj
                      (mk y) ≅
                    ((Functor.obj Functor.curry₃
                              (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                                inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                          (mk x)).obj
                      (mk y)))
              y₀) ≫
          ((Functor.obj Functor.curry₃
                    (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                      inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                (mk x)).map
            (homMk e))
        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)).map
        (homMk e) ≫
      Iso.hom
        ((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)).obj
                  (mk y) ≅
                ((Functor.obj Functor.curry₃
                          (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                            inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                      (mk x)).obj
                  (mk y)))
          y₁) =
    Iso.hom
        ((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)).obj
                  (mk y) ≅
                ((Functor.obj Functor.curry₃
                          (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                            inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                      (mk x)).obj
                  (mk y)))
          y₀) ≫
      ((Functor.obj Functor.curry₃
                (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                  inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
            (mk x)).map
        (homMk e)

Tactic:
ext z