-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
x₀ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge (X := tensorObj (𝒞 := Functor.category) X Y) (x₀, y₀) (x₁, y₁)
obtain :
  ∀ (ex : Edge x₀ x₁) (ey : Edge y₀ y₁),
    Eq (α :=
      (functor X Y ⋙ inverse X Y).obj (mk (x₀, y₀)) ⟶
        Functor.obj (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (mk (x₁, y₁)))
      ((functor X Y ⋙ inverse X Y).map (homMk (ex.tensor ey)) ≫
        Iso.hom
          ((fun
                (x :
                  (tensorObj (𝒞 := Functor.category) X Y).obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk x)) :
                (functor X Y ⋙ inverse X Y).obj (mk x) ≅ (functor X Y ⋙ inverse X Y).obj (mk x)))
            (x₁, y₁)))
      (Iso.hom
          ((fun
                (x :
                  (tensorObj (𝒞 := Functor.category) X Y).obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk x)) :
                (functor X Y ⋙ inverse X Y).obj (mk x) ≅ (functor X Y ⋙ inverse X Y).obj (mk x)))
            (x₀, y₀)) ≫
        CategoryTheory.Functor.map (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (homMk (ex.tensor ey)))
⊢ Eq (α :=
    (functor X Y ⋙ inverse X Y).obj (mk (x₀, y₀)) ⟶
      Functor.obj (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (mk (x₁, y₁)))
    ((functor X Y ⋙ inverse X Y).map (homMk e) ≫
      Iso.hom
        ((fun
              (x :
                (tensorObj (𝒞 := Functor.category) X Y).obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk x)) :
              (functor X Y ⋙ inverse X Y).obj (mk x) ≅ (functor X Y ⋙ inverse X Y).obj (mk x)))
          (x₁, y₁)))
    (Iso.hom
        ((fun
              (x :
                (tensorObj (𝒞 := Functor.category) X Y).obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk x)) :
              (functor X Y ⋙ inverse X Y).obj (mk x) ≅ (functor X Y ⋙ inverse X Y).obj (mk x)))
          (x₀, y₀)) ≫
      CategoryTheory.Functor.map (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (homMk e))

Tactic:
obtain ⟨ex, ey, rfl⟩ := e.tensor_surjective

Premises used: SSet.Truncated.Edge.tensor_surjective, rfl