-- 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₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge y₀ 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₀)
        (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₁)))
    (CategoryTheory.Functor.map
        ((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₀)
        (homMk e') ≫
      (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)))
        y₁)
    ((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)))
        y₀ ≫
      CategoryTheory.Functor.map
        ((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₁)
        (homMk e'))

Tactic:
simp [square]

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.square