-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ 𝟙
        ((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)
have 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)))
                    sorry)
                sorry)
            sorry)))
      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: rw [Category.id_comp, Category.comp_id]