-- 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₁
⊢ Eq (α :=
    (Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₀) ⟶
      Functor.obj (Functor.obj Functor.curry (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)) (mk x₁))
    ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (snd 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 ⋙ mapHomotopyCategory (snd X Y))).obj (mk x)).obj (mk y)))
              ⋯)
          x₁))
    (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 ⋙ mapHomotopyCategory (snd X Y))).obj (mk x)).obj (mk y)))
              ⋯)
          x₀) ≫
      CategoryTheory.Functor.map
        (Functor.obj Functor.curry (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)) (homMk e))
have w : ∀ (y : Y.HomotopyCategory),
  Eq (α :=
    ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₀)).obj y ⟶
      Functor.obj
        (Functor.obj (Functor.obj Functor.curry (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory))
          (mk x₁))
        y)
    (NatTrans.app
      ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (snd 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 ⋙ mapHomotopyCategory (snd X Y))).obj (mk x)).obj (mk y)))
                sorry)
            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 ⋙ mapHomotopyCategory (snd X Y))).obj (mk x)).obj (mk y)))
                sorry)
            x₀) ≫
        CategoryTheory.Functor.map
          (Functor.obj Functor.curry (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)) (homMk e))
      y)
Tactic: ext y