-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
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.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
z₀ z₁ :
  Z.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge z₀ z₁
⊢ 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
        (mk 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
        (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)).map
        (homMk e) ≫
      Iso.hom
        ((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)).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)).obj
                  (mk z)))
          z₁))
    (Iso.hom
        ((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)).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)).obj
                  (mk z)))
          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)).map
        (homMk e))
have dsimp : Eq (α :=
  (((Functor.obj Functor.curry₃
                  (prod.inverseAssociator 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₃
                  (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                    inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
              (mk x)).obj
          (mk y)).obj
      (mk z₁))
  (CategoryTheory.Functor.map (mapHomotopyCategory (Iso.hom (α_ X Y Z)))
        (CategoryTheory.Functor.map (inverse (tensorObj (𝒞 := Functor.category) X Y) Z)
          (Prod.mkHom ((inverse X Y).map (Prod.mkHom (𝟙 (mk x)) (𝟙 (mk y)))) (homMk e))) ≫
      𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator 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₃
                    (prod.inverseAssociator 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₃
                    (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                      inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                (mk x)).obj
            (mk y)).obj
        (mk z₁))
  (𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator 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₀)) ≫
      CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
        (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (𝟙 (mk y), homMk e))) :
    (((Functor.obj Functor.curry₃
                    (prod.inverseAssociator 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₃
                    (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                      inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                (mk x)).obj
            (mk y)).obj
        (mk z₁))
Tactic: dsimp