-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y Z : Functor.{v, v', u, u'} C D
x : X_1 ⟶ Y
x_1 : Y ⟶ Z
w :
  ∀ (x_2 : Augmented.{v, u} C) (n : SimplexCategoryᵒᵖ),
    ({
                  app := fun (A : Augmented.{v, u} C) ↦
                    { left := whiskerLeft (obj drop A) (x ≫ x_1), right := (x ≫ x_1).app (obj point A), w := ⋯ :
                      CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Z).obj A) },
                  naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Z) }.app
              x_2).left.app
        n =
      NatTrans.app
        (CommaMorphism.left
          (NatTrans.app
            ({
                app := fun (A : Augmented.{v, u} C) ↦
                  { left := whiskerLeft (obj drop A) x, right := x.app (obj point A), w := ⋯ :
                    CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Y).obj A) },
                naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Y) } ≫
              {
                app := fun (A : Augmented.{v, u} C) ↦
                  { left := whiskerLeft (obj drop A) x_1, right := x_1.app (obj point A), w := ⋯ },
                naturality := ⋯ })
            x_2))
        n
⊢ {
      app := fun (A : Augmented.{v, u} C) ↦
        { left := whiskerLeft (obj drop A) (x ≫ x_1), right := (x ≫ x_1).app (obj point A), w := ⋯ :
          CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Z).obj A) },
      naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Z) } =
    {
        app := fun (A : Augmented.{v, u} C) ↦
          { left := whiskerLeft (obj drop A) x, right := x.app (obj point A), w := ⋯ :
            CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Y).obj A) },
        naturality := ⋯ : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Y) } ≫
      {
        app := fun (A : Augmented.{v, u} C) ↦
          { left := whiskerLeft (obj drop A) x_1, right := x_1.app (obj point A), w := ⋯ },
        naturality := ⋯ }
have w₁ : ∀ (x_2 : Augmented.{v, u} C),
  ({
            app := fun (A : Augmented.{v, u} C) ↦
              { left := whiskerLeft (obj drop A) (x ≫ x_1), right := (x ≫ x_1).app (obj point A), w := sorry :
                CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Z).obj A) },
            naturality := sorry : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Z) }.app
        x_2).right =
    CommaMorphism.right
      (NatTrans.app
        ({
            app := fun (A : Augmented.{v, u} C) ↦
              { left := whiskerLeft (obj drop A) x, right := x.app (obj point A), w := sorry :
                CommaMorphism ((whiskeringObj C D X_1).obj A) ((whiskeringObj C D Y).obj A) },
            naturality := sorry : NatTrans (whiskeringObj C D X_1) (whiskeringObj C D Y) } ≫
          {
            app := fun (A : Augmented.{v, u} C) ↦
              { left := whiskerLeft (obj drop A) x_1, right := x_1.app (obj point A), w := sorry },
            naturality := sorry })
        x_2)
Tactic: ext