-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ Eq (α :=
    (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
        xyz ⟶
      (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙ inverse X (tensorObj (𝒞 := Functor.category) Y Z)).obj xyz)
    (NatTrans.app
        (CategoryTheory.Functor.map (Equivalence.functor Functor.currying₃)
          (Iso.hom
            (mkNatIso
              (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)))
                      ⋯)
                  ⋯)
              ⋯)))
        xyz :
      (Functor.obj (Equivalence.inverse Functor.currying₃ ⋙ Equivalence.functor Functor.currying₃)
              (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
          xyz ⟶
        (Functor.obj (Equivalence.functor Functor.currying₃)
              (Functor.obj (Equivalence.inverse Functor.currying₃)
                (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                  inverse X (tensorObj (𝒞 := Functor.category) Y Z)))).obj
          xyz)
    (𝟙
        ((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
          xyz) :
      (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
          xyz ⟶
        (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
          xyz)

Tactic:
rfl