Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ (((Functor.curry₃.obj
                    ((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
                      (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                        inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).map
                (homMk e) ≫
              (mkNatIso
                  (fun y ↦
                    mkNatIso
                      (fun z ↦
                        Iso.refl
                          ((((Functor.curry₃.obj
                                        ((prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                              Z.HomotopyCategory).inverse ⋙
                                          (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                            inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                                    (mk x₁)).obj
                                (mk y)).obj
                            (mk z)))
                      ⋯)
                  ⋯).hom).app
          (mk y)).app
      (mk z) =
    (((mkNatIso
                  (fun y ↦
                    mkNatIso
                      (fun z ↦
                        Iso.refl
                          ((((Functor.curry₃.obj
                                        ((prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                              Z.HomotopyCategory).inverse ⋙
                                          (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                            inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                                    (mk x₀)).obj
                                (mk y)).obj
                            (mk z)))
                      ⋯)
                  ⋯).hom ≫
              (Functor.curry₃.obj ((𝟭 X.HomotopyCategory).prod (inverse Y Z) ⋙ inverse X (Y ⊗ Z))).map (homMk e)).app
          (mk y)).app
      (mk z)

Tactic:
dsimp

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk (e.tensor (Edge.id (y, z))) ≫
      𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x₁)).obj
              (mk y)).obj
          (mk z)) =
    𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x₀)).obj
              (mk y)).obj
          (mk z)) ≫
      (inverse X (Y ⊗ Z)).map (Prod.mkHom (homMk e) ((inverse Y Z).map (𝟙 (mk y), 𝟙 (mk z))))