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₁
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

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

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.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)).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
      (mk 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
      (mk z)