-- 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.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))

Tactic:
simpa using homMk_comp_homMk (h.tensor (.idCompId y))

Premises used: SSet.Truncated.Edge.CompStruct.tensor, SSet.Truncated.Edge.CompStruct.idCompId, SSet.Truncated.HomotopyCategory.homMk_comp_homMk