-- 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₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge y₀ y₁
dsimp :
  homMk (Edge.id x) ≫
      𝟙
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (fst
                  (X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1)))
                  (Y.obj
                    (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 }))
            (x, y₁))) =
    𝟙
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (fst
                  (X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1)))
                  (Y.obj
                    (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 }))
            (x, y₀))) ≫
      𝟙 (mk x)
⊢ Eq (α :=
    ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y₀) ⟶
      Functor.obj
        (Functor.obj (Functor.obj Functor.curry (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)) (mk x))
        (mk y₁))
    (((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).map (homMk e) ≫
      Iso.hom
        ((fun
              (y :
                Y.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (Iso.refl
                (((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y)) :
              ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y) ≅
                ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y)))
          y₁))
    (Iso.hom
        ((fun
              (y :
                Y.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (Iso.refl
                (((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y)) :
              ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y) ≅
                ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y)))
          y₀) ≫
      CategoryTheory.Functor.map
        (Functor.obj (Functor.obj Functor.curry (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)) (mk x))
        (homMk e))

Tactic:
dsimp