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

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Premises used: SSet.Truncated.HomotopyCategory.mk_surjective, rfl