-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
f : X ⟶ X'
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 (α :=
    ((Functor.obj Functor.curry ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj (mk x₀)).obj
        (mk y) ⟶
      ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).obj (mk x₁)).obj (mk y))
    (NatTrans.app
      ((Functor.obj Functor.curry ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).map (homMk e) ≫
        Iso.hom
          ((fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (mkNatIso
                  (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
                                ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                            (mk x)).obj
                        (mk y)))
                  ⋯ :
                (Functor.obj Functor.curry ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x) ≅
                  (Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).obj (mk x)))
            x₁))
      (mk y))
    (NatTrans.app
      (Iso.hom
          ((fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (mkNatIso
                  (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
                                ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                            (mk x)).obj
                        (mk y)))
                  ⋯ :
                (Functor.obj Functor.curry ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x) ≅
                  (Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).obj (mk x)))
            x₀) ≫
        (Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).map (homMk e))
      (mk y))
have w : homMk ((e.map f).tensor (Edge.id y)) ≫
    𝟙
      (mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (f.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 })) →
                X'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
            x₁,
          y)) =
  𝟙
      (mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (f.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 })) →
                X'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
            x₀,
          y)) ≫
    homMk ((e.map f).tensor (Edge.id y))
Tactic: simp