-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
rw :
  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)
⊢ 𝟙
        ((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)

Tactic:
rw [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp