-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
y : Y.HomotopyCategory
w :
  ∀
    (y :
      Y.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    Eq (α :=
      Quiver.Hom (V := (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
        (Functor.obj
          ((fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (lift
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    mk (x, y))
                  (fun
                      {y₀ y₁ :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))}
                      (e : Edge y₀ y₁) ↦
                    homMk ((Edge.id x).tensor e))
                  ⋯ ⋯ :
                Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
            x₀)
          (mk y))
        (Functor.obj
          ((fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (lift
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    mk (x, y))
                  (fun
                      {y₀ y₁ :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))}
                      (e : Edge y₀ y₁) ↦
                    homMk ((Edge.id x).tensor e))
                  ⋯ ⋯ :
                Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
            x₂)
          (mk y)))
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          (fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (lift
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    mk (x, y))
                  (fun
                      {y₀ y₁ :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))}
                      (e : Edge y₀ y₁) ↦
                    homMk ((Edge.id x).tensor e))
                  ⋯ ⋯ :
                Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
            x₁)
          ((fun
                {x₀ x₁ :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))}
                (e : Edge x₀ x₁) ↦
              (mkNatTrans
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    homMk (e.tensor (Edge.id y)))
                  ⋯ :
                Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
                  ((fun
                        (x :
                          X.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      (lift
                          (fun
                              (y :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            mk (x, y))
                          (fun
                              {y₀ y₁ :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))}
                              (e : Edge y₀ y₁) ↦
                            homMk ((Edge.id x).tensor e))
                          ⋯ ⋯ :
                        Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                    x₀)
                  ((fun
                        (x :
                          X.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      (lift
                          (fun
                              (y :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            mk (x, y))
                          (fun
                              {y₀ y₁ :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))}
                              (e : Edge y₀ y₁) ↦
                            homMk ((Edge.id x).tensor e))
                          ⋯ ⋯ :
                        Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                    x₁)))
            e₀₁)
          ((fun
                {x₀ x₁ :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))}
                (e : Edge x₀ x₁) ↦
              (mkNatTrans
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    homMk (e.tensor (Edge.id y)))
                  ⋯ :
                Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
                  ((fun
                        (x :
                          X.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      (lift
                          (fun
                              (y :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            mk (x, y))
                          (fun
                              {y₀ y₁ :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))}
                              (e : Edge y₀ y₁) ↦
                            homMk ((Edge.id x).tensor e))
                          ⋯ ⋯ :
                        Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                    x₀)
                  ((fun
                        (x :
                          X.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      (lift
                          (fun
                              (y :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            mk (x, y))
                          (fun
                              {y₀ y₁ :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))}
                              (e : Edge y₀ y₁) ↦
                            homMk ((Edge.id x).tensor e))
                          ⋯ ⋯ :
                        Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                    x₁)))
            e₁₂))
        (mk y))
      (NatTrans.app
        ((fun
              {x₀ x₁ :
                X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))}
              (e : Edge x₀ x₁) ↦
            (mkNatTrans
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  homMk (e.tensor (Edge.id y)))
                ⋯ :
              Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
                ((fun
                      (x :
                        X.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    (lift
                        (fun
                            (y :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))) ↦
                          mk (x, y))
                        (fun
                            {y₀ y₁ :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))}
                            (e : Edge y₀ y₁) ↦
                          homMk ((Edge.id x).tensor e))
                        ⋯ ⋯ :
                      Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                  x₀)
                ((fun
                      (x :
                        X.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    (lift
                        (fun
                            (y :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))) ↦
                          mk (x, y))
                        (fun
                            {y₀ y₁ :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))}
                            (e : Edge y₀ y₁) ↦
                          homMk ((Edge.id x).tensor e))
                        ⋯ ⋯ :
                      Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                  x₁)))
          e₀₂)
        (mk y))
⊢ Eq (α :=
    Quiver.Hom (V := (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
      (Functor.obj
        ((fun
              (x :
                X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (lift
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  mk (x, y))
                (fun
                    {y₀ y₁ :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))}
                    (e : Edge y₀ y₁) ↦
                  homMk ((Edge.id x).tensor e))
                ⋯ ⋯ :
              Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
          x₀)
        y)
      (Functor.obj
        ((fun
              (x :
                X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (lift
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  mk (x, y))
                (fun
                    {y₀ y₁ :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))}
                    (e : Edge y₀ y₁) ↦
                  homMk ((Edge.id x).tensor e))
                ⋯ ⋯ :
              Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
          x₂)
        y))
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        (fun
              (x :
                X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (lift
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  mk (x, y))
                (fun
                    {y₀ y₁ :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))}
                    (e : Edge y₀ y₁) ↦
                  homMk ((Edge.id x).tensor e))
                ⋯ ⋯ :
              Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
          x₁)
        ((fun
              {x₀ x₁ :
                X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))}
              (e : Edge x₀ x₁) ↦
            (mkNatTrans
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  homMk (e.tensor (Edge.id y)))
                ⋯ :
              Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
                ((fun
                      (x :
                        X.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    (lift
                        (fun
                            (y :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))) ↦
                          mk (x, y))
                        (fun
                            {y₀ y₁ :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))}
                            (e : Edge y₀ y₁) ↦
                          homMk ((Edge.id x).tensor e))
                        ⋯ ⋯ :
                      Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                  x₀)
                ((fun
                      (x :
                        X.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    (lift
                        (fun
                            (y :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))) ↦
                          mk (x, y))
                        (fun
                            {y₀ y₁ :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))}
                            (e : Edge y₀ y₁) ↦
                          homMk ((Edge.id x).tensor e))
                        ⋯ ⋯ :
                      Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                  x₁)))
          e₀₁)
        ((fun
              {x₀ x₁ :
                X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))}
              (e : Edge x₀ x₁) ↦
            (mkNatTrans
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  homMk (e.tensor (Edge.id y)))
                ⋯ :
              Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
                ((fun
                      (x :
                        X.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    (lift
                        (fun
                            (y :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))) ↦
                          mk (x, y))
                        (fun
                            {y₀ y₁ :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))}
                            (e : Edge y₀ y₁) ↦
                          homMk ((Edge.id x).tensor e))
                        ⋯ ⋯ :
                      Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                  x₀)
                ((fun
                      (x :
                        X.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    (lift
                        (fun
                            (y :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))) ↦
                          mk (x, y))
                        (fun
                            {y₀ y₁ :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))}
                            (e : Edge y₀ y₁) ↦
                          homMk ((Edge.id x).tensor e))
                        ⋯ ⋯ :
                      Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                  x₁)))
          e₁₂))
      y)
    (NatTrans.app
      ((fun
            {x₀ x₁ :
              X.obj
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))}
            (e : Edge x₀ x₁) ↦
          (mkNatTrans
              (fun
                  (y :
                    Y.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                homMk (e.tensor (Edge.id y)))
              ⋯ :
            Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
              ((fun
                    (x :
                      X.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  (lift
                      (fun
                          (y :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))) ↦
                        mk (x, y))
                      (fun
                          {y₀ y₁ :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))}
                          (e : Edge y₀ y₁) ↦
                        homMk ((Edge.id x).tensor e))
                      ⋯ ⋯ :
                    Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                x₀)
              ((fun
                    (x :
                      X.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  (lift
                      (fun
                          (y :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))) ↦
                        mk (x, y))
                      (fun
                          {y₀ y₁ :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))}
                          (e : Edge y₀ y₁) ↦
                        homMk ((Edge.id x).tensor e))
                      ⋯ ⋯ :
                    Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                x₁)))
        e₀₂)
      y)

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

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