-- Mathlib/CategoryTheory/Functor/TwoSquare.lean
/-- When composing 2-squares which form a diagram of grid, compositing horionzall first yields the
same result as composing vertically first. -/
lemma hCompVCompHComp (w₁ : TwoSquare T L R B) (w₂ : TwoSquare T' R R' B')
    (w₃ : TwoSquare B L' R'' B'') (w₄ : TwoSquare B' R'' R₃ B₃) :
    (w₁ ≫ₕ w₂) ≫ᵥ (w₃ ≫ₕ w₄) = (w₁ ≫ᵥ w₃) ≫ₕ (w₂ ≫ᵥ w₄)

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₃, u₃} C₃
inst✝⁵ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst✝⁴ : Category.{v₅, u₅} C₅
inst✝³ : Category.{v₆, u₆} C₆
inst✝² : Category.{v₇, u₇} C₇
inst✝¹ : Category.{v₈, u₈} C₈
T' : C₂ ⥤ C₅
R' : C₅ ⥤ C₆
B' : C₄ ⥤ C₆
L' : C₃ ⥤ C₇
R'' : C₄ ⥤ C₈
B'' : C₇ ⥤ C₈
C₉ : Type u₉
inst✝ : Category.{v₉, u₉} C₉
R₃ : C₆ ⥤ C₉
B₃ : C₈ ⥤ C₉
w₁ : TwoSquare T L R B
w₂ : TwoSquare T' R R' B'
w₃ : TwoSquare B L' R'' B''
w₄ : TwoSquare B' R'' R₃ B₃
⊢ mk (T ⋙ T') (L ⋙ L') (R' ⋙ R₃) (B'' ⋙ B₃)
      (((T ⋙ T').associator R' R₃).hom ≫
        {
            app := fun X =>
              R₃.map
                ((mk (T ⋙ T') L R' (B ⋙ B')
                        ((T.associator T' R').hom ≫
                          { app := fun X => w₂.natTrans.app (T.obj X), naturality := ⋯ } ≫
                            (T.associator R B').inv ≫
                              { app := fun X => B'.map (w₁.natTrans.app X), naturality := ⋯ } ≫
                                (L.associator B B').hom)).natTrans.app
                  X),
            naturality := ⋯ } ≫
          (L.associator (B ⋙ B') R₃).inv ≫
            {
                app := fun X =>
                  (mk (B ⋙ B') L' R₃ (B'' ⋙ B₃)
                          ((B.associator B' R₃).hom ≫
                            { app := fun X => w₄.natTrans.app (B.obj X), naturality := ⋯ } ≫
                              (B.associator R'' B₃).inv ≫
                                { app := fun X => B₃.map (w₃.natTrans.app X), naturality := ⋯ } ≫
                                  (L'.associator B'' B₃).hom)).natTrans.app
                    (L.obj X),
                naturality := ⋯ } ≫
              (L.associator L' (B'' ⋙ B₃)).hom) =
    mk (T ⋙ T') (L ⋙ L') (R' ⋙ R₃) (B'' ⋙ B₃)
      ((T.associator T' (R' ⋙ R₃)).hom ≫
        {
            app := fun X =>
              (mk T' (R ⋙ R'') (R' ⋙ R₃) B₃
                      ((T'.associator R' R₃).hom ≫
                        { app := fun X => R₃.map (w₂.natTrans.app X), naturality := ⋯ } ≫
                          (R.associator B' R₃).inv ≫
                            { app := fun X => w₄.natTrans.app (R.obj X), naturality := ⋯ } ≫
                              (R.associator R'' B₃).hom)).natTrans.app
                (T.obj X),
            naturality := ⋯ } ≫
          (T.associator (R ⋙ R'') B₃).inv ≫
            {
                app := fun X =>
                  B₃.map
                    ((mk T (L ⋙ L') (R ⋙ R'') B''
                            ((T.associator R R'').hom ≫
                              { app := fun X => R''.map (w₁.natTrans.app X), naturality := ⋯ } ≫
                                (L.associator B R'').inv ≫
                                  { app := fun X => w₃.natTrans.app (L.obj X), naturality := ⋯ } ≫
                                    (L.associator L' B'').hom)).natTrans.app
                      X),
                naturality := ⋯ } ≫
              ((L ⋙ L').associator B'' B₃).hom)

Tactic:
ext c

Result:
case h
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₃, u₃} C₃
inst✝⁵ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst✝⁴ : Category.{v₅, u₅} C₅
inst✝³ : Category.{v₆, u₆} C₆
inst✝² : Category.{v₇, u₇} C₇
inst✝¹ : Category.{v₈, u₈} C₈
T' : C₂ ⥤ C₅
R' : C₅ ⥤ C₆
B' : C₄ ⥤ C₆
L' : C₃ ⥤ C₇
R'' : C₄ ⥤ C₈
B'' : C₇ ⥤ C₈
C₉ : Type u₉
inst✝ : Category.{v₉, u₉} C₉
R₃ : C₆ ⥤ C₉
B₃ : C₈ ⥤ C₉
w₁ : TwoSquare T L R B
w₂ : TwoSquare T' R R' B'
w₃ : TwoSquare B L' R'' B''
w₄ : TwoSquare B' R'' R₃ B₃
c : C₁
⊢ (mk (T ⋙ T') (L ⋙ L') (R' ⋙ R₃) (B'' ⋙ B₃)
            (((T ⋙ T').associator R' R₃).hom ≫
              {
                  app := fun X =>
                    R₃.map
                      ((mk (T ⋙ T') L R' (B ⋙ B')
                              ((T.associator T' R').hom ≫
                                { app := fun X => w₂.natTrans.app (T.obj X), naturality := ⋯ } ≫
                                  (T.associator R B').inv ≫
                                    { app := fun X => B'.map (w₁.natTrans.app X), naturality := ⋯ } ≫
                                      (L.associator B B').hom)).natTrans.app
                        X),
                  naturality := ⋯ } ≫
                (L.associator (B ⋙ B') R₃).inv ≫
                  {
                      app := fun X =>
                        (mk (B ⋙ B') L' R₃ (B'' ⋙ B₃)
                                ((B.associator B' R₃).hom ≫
                                  { app := fun X => w₄.natTrans.app (B.obj X), naturality := ⋯ } ≫
                                    (B.associator R'' B₃).inv ≫
                                      { app := fun X => B₃.map (w₃.natTrans.app X), naturality := ⋯ } ≫
                                        (L'.associator B'' B₃).hom)).natTrans.app
                          (L.obj X),
                      naturality := ⋯ } ≫
                    (L.associator L' (B'' ⋙ B₃)).hom)).natTrans.app
      c =
    (mk (T ⋙ T') (L ⋙ L') (R' ⋙ R₃) (B'' ⋙ B₃)
            ((T.associator T' (R' ⋙ R₃)).hom ≫
              {
                  app := fun X =>
                    (mk T' (R ⋙ R'') (R' ⋙ R₃) B₃
                            ((T'.associator R' R₃).hom ≫
                              { app := fun X => R₃.map (w₂.natTrans.app X), naturality := ⋯ } ≫
                                (R.associator B' R₃).inv ≫
                                  { app := fun X => w₄.natTrans.app (R.obj X), naturality := ⋯ } ≫
                                    (R.associator R'' B₃).hom)).natTrans.app
                      (T.obj X),
                  naturality := ⋯ } ≫
                (T.associator (R ⋙ R'') B₃).inv ≫
                  {
                      app := fun X =>
                        B₃.map
                          ((mk T (L ⋙ L') (R ⋙ R'') B''
                                  ((T.associator R R'').hom ≫
                                    { app := fun X => R''.map (w₁.natTrans.app X), naturality := ⋯ } ≫
                                      (L.associator B R'').inv ≫
                                        { app := fun X => w₃.natTrans.app (L.obj X), naturality := ⋯ } ≫
                                          (L.associator L' B'').hom)).natTrans.app
                            X),
                      naturality := ⋯ } ≫
                    ((L ⋙ L').associator B'' B₃).hom)).natTrans.app
      c