-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic
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
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 := ⋯ :
                  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).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 := ⋯ :
                  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)
⊢ {
      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 := ⋯ }

Tactic:
ext