-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
z : Z.HomotopyCategory
y :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ 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
        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
        z)
    (NatTrans.app
      (NatTrans.app
        ((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)))).map
            (homMk e) ≫
          Iso.hom
            ((fun
                  (x :
                    X.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (mkNatIso
                    (fun
                        (y :
                          Y.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      mkNatIso
                        (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) ≅
                    (Functor.obj Functor.curry₃
                          (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                            inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                      (mk x)))
              x₁))
        (mk y))
      z)
    (NatTrans.app
      (NatTrans.app
        (Iso.hom
            ((fun
                  (x :
                    X.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (mkNatIso
                    (fun
                        (y :
                          Y.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      mkNatIso
                        (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) ≅
                    (Functor.obj Functor.curry₃
                          (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                            inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                      (mk x)))
              x₀) ≫
          (Functor.obj Functor.curry₃
                (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                  inverse X (tensorObj (𝒞 := Functor.category) Y Z))).map
            (homMk e))
        (mk y))
      z)
have w : ∀
  (z :
    Z.obj
      (Opposite.op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))),
  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))
    (NatTrans.app
      (NatTrans.app
        ((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)))).map
            (homMk e) ≫
          Iso.hom
            ((fun
                  (x :
                    X.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (mkNatIso
                    (fun
                        (y :
                          Y.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      mkNatIso
                        (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)))
                        sorry)
                    sorry :
                  (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) ≅
                    (Functor.obj Functor.curry₃
                          (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                            inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                      (mk x)))
              x₁))
        (mk y))
      (mk z))
    (NatTrans.app
      (NatTrans.app
        (Iso.hom
            ((fun
                  (x :
                    X.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (mkNatIso
                    (fun
                        (y :
                          Y.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      mkNatIso
                        (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)))
                        sorry)
                    sorry :
                  (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) ≅
                    (Functor.obj Functor.curry₃
                          (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                            inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                      (mk x)))
              x₀) ≫
          (Functor.obj Functor.curry₃
                (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                  inverse X (tensorObj (𝒞 := Functor.category) Y Z))).map
            (homMk e))
        (mk y))
      (mk z))
Tactic: obtain ⟨z, rfl⟩ := z.mk_surjective
Cleared hypotheses: z