-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
change :
  𝟙
        ((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) ≫
      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.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)
⊢ (associativity'Iso X Y Z).hom.app 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:
change 𝟙 _ ≫ _ ≫ 𝟙 _ = _

Premises used: CategoryTheory.CategoryStruct.id