-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
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₁
⊢ 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))
have 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)
Tactic: dsimp