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₁
z : Z.HomotopyCategory
y : Y.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
      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
      z

Tactic:
obtain ⟨z, rfl⟩ := z.mk_surjective

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 })
⊢ (((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)