-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
w :
  ∀ (y : Y.HomotopyCategory),
    NatTrans.app
        ((Functor.obj Functor.curry (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ 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
                                (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                            (mk x)).obj
                        (mk y)))
                  ⋯)
              x₁))
        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
                                (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                            (mk x)).obj
                        (mk y)))
                  ⋯)
              x₀) ≫
          (Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e))
        y
⊢ (Functor.obj Functor.curry (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ 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
                            (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                        (mk x)).obj
                    (mk y)))
              ⋯)
          x₁) =
    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
                            (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                        (mk x)).obj
                    (mk y)))
              ⋯)
          x₀) ≫
      (Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e)

Tactic:
ext y