Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
⊢ ((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)).map
        (homMk e) ≫
      (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 =
    (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))).obj (mk x)).map (homMk e)

Tactic:
ext z

Goal state after:
X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
z : Z.HomotopyCategory
⊢ (((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)).map
            (homMk e) ≫
          (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
      z =
    ((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))).obj (mk x)).map
            (homMk e)).app
      z