-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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₁
w :
  ∀ (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)
⊢ Eq (α :=
    (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₁))
    ((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₁))
    (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))

Tactic:
ext y : 2