-- 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₁
y : Y.HomotopyCategory
⊢ Eq (α :=
    ((Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x₀)).obj y ⟶
      Functor.obj (Functor.obj (Functor.obj Functor.curry (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))) (mk x₁)) y)
    (NatTrans.app
      ((Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).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))) ↦
                    Iso.refl (((Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x)).obj (mk y)))
                  ⋯ :
                (Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x) ≅
                  Functor.obj (Functor.obj Functor.curry (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))) (mk x)))
            x₁))
      y)
    (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))) ↦
                    Iso.refl (((Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x)).obj (mk y)))
                  ⋯ :
                (Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x) ≅
                  Functor.obj (Functor.obj Functor.curry (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))) (mk x)))
            x₀) ≫
        CategoryTheory.Functor.map (Functor.obj Functor.curry (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))) (homMk e))
      y)
have w : ∀
  (y :
    Y.obj
      (Opposite.op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))),
  Eq (α :=
    ((Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x₀)).obj (mk y) ⟶
      Functor.obj (Functor.obj (Functor.obj Functor.curry (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))) (mk x₁))
        (mk y))
    (NatTrans.app
      ((Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).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))) ↦
                    Iso.refl (((Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x)).obj (mk y)))
                  sorry :
                (Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x) ≅
                  Functor.obj (Functor.obj Functor.curry (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))) (mk x)))
            x₁))
      (mk y))
    (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))) ↦
                    Iso.refl (((Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x)).obj (mk y)))
                  sorry :
                (Functor.obj Functor.curry (inverse X Y ⋙ functor X Y)).obj (mk x) ≅
                  Functor.obj (Functor.obj Functor.curry (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))) (mk x)))
            x₀) ≫
        CategoryTheory.Functor.map (Functor.obj Functor.curry (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))) (homMk e))
      (mk y))
Tactic: obtain ⟨y, rfl⟩ := y.mk_surjective
Cleared hypotheses: y