-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
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₀₂
⊢ Eq.{u + 1} (α :=
    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₂))
    (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₁₂))
    ((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₀₂)
have w : ∀ (y : Y.HomotopyCategory),
  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))
                sorry sorry :
              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))
                sorry sorry :
              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))
                sorry sorry :
              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)))
                sorry :
              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))
                        sorry sorry :
                      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))
                        sorry sorry :
                      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)))
                sorry :
              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))
                        sorry sorry :
                      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))
                        sorry sorry :
                      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)))
              sorry :
            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))
                      sorry sorry :
                    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))
                      sorry sorry :
                    Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                x₁)))
        e₀₂)
      y)
Tactic: ext y