-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
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.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)
      (mk
        (x₀,
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (g.app
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) :
              (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
                Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
            y))
      (mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1)) ◁
                g.app
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) :
            (a :
                X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) ⊗
                  Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
              X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) ⊗
                Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
          (x₁, y))))
    (homMk
        (e.tensor
          (Edge.id
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (g.app
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) :
                (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
                  Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
              y))) ≫
      𝟙
        (mk
          (x₁,
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (g.app
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) :
                (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
                  Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
              y)))
    (𝟙
        (mk
          (x₀,
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (g.app
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) :
                (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
                  Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
              y)) ≫
      homMk
        (e.tensor
          (Edge.id
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (g.app
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        Edge._proof_1))) :
                (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })) →
                  Y'.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
              y))))

Tactic:
rfl