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