-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.TwoSquare (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst_4 : Category.{v₅, u₅} C₅
inst_5 : Category.{v₆, u₆} C₆
inst_6 : Category.{v₇, u₇} C₇
inst_7 : Category.{v₈, u₈} C₈
T' : Functor.{v₂, v₅, u₂, u₅} C₂ C₅
R' : Functor.{v₅, v₆, u₅, u₆} C₅ C₆
B' : Functor.{v₄, v₆, u₄, u₆} C₄ C₆
L' : Functor.{v₃, v₇, u₃, u₇} C₃ C₇
R'' : Functor.{v₄, v₈, u₄, u₈} C₄ C₈
B'' : Functor.{v₇, v₈, u₇, u₈} C₇ C₈
C₉ : Type u₉
inst_8 : Category.{v₉, u₉} C₉
R₃ : Functor.{v₆, v₉, u₆, u₉} C₆ C₉
B₃ : Functor.{v₈, v₉, u₈, u₉} 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₃).inv ≫
        {
            app := fun (X : C₁) ↦
              R₃.map
                ((mk (T ⋙ T') L R' (B ⋙ B')
                        ((T.associator T' R').hom ≫
                          { app := fun (X : C₁) ↦ w₂.natTrans.app (T.obj X), naturality := ⋯ :
                              NatTrans (T ⋙ T' ⋙ R') (T ⋙ R ⋙ B') } ≫
                            (T.associator R B').inv ≫
                              { app := fun (X : C₁) ↦ B'.map (w₁.natTrans.app X), naturality := ⋯ :
                                  NatTrans ((T ⋙ R) ⋙ B') ((L ⋙ B) ⋙ B') } ≫
                                (L.associator B B').hom)).natTrans.app
                  X),
            naturality := ⋯ : NatTrans (((T ⋙ T') ⋙ R') ⋙ R₃) ((L ⋙ B ⋙ B') ⋙ R₃) } ≫
          (L.associator (B ⋙ B') R₃).hom ≫
            {
                app := fun (X : C₁) ↦
                  (mk (B ⋙ B') L' R₃ (B'' ⋙ B₃)
                          ((B.associator B' R₃).hom ≫
                            { app := fun (X : C₃) ↦ w₄.natTrans.app (B.obj X), naturality := ⋯ :
                                NatTrans (B ⋙ B' ⋙ R₃) (B ⋙ R'' ⋙ B₃) } ≫
                              (B.associator R'' B₃).inv ≫
                                { app := fun (X : C₃) ↦ B₃.map (w₃.natTrans.app X), naturality := ⋯ :
                                    NatTrans ((B ⋙ R'') ⋙ B₃) ((L' ⋙ B'') ⋙ B₃) } ≫
                                  (L'.associator B'' B₃).hom)).natTrans.app
                    (L.obj X),
                naturality := ⋯ : NatTrans (L ⋙ (B ⋙ B') ⋙ R₃) (L ⋙ L' ⋙ B'' ⋙ B₃) } ≫
              (L.associator L' (B'' ⋙ B₃)).inv) =
    mk (T ⋙ T') (L ⋙ L') (R' ⋙ R₃) (B'' ⋙ B₃)
      ((T.associator T' (R' ⋙ R₃)).hom ≫
        {
            app := fun (X : C₁) ↦
              (mk T' (R ⋙ R'') (R' ⋙ R₃) B₃
                      ((T'.associator R' R₃).inv ≫
                        { app := fun (X : C₂) ↦ R₃.map (w₂.natTrans.app X), naturality := ⋯ } ≫
                          (R.associator B' R₃).hom ≫
                            { app := fun (X : C₂) ↦ w₄.natTrans.app (R.obj X), naturality := ⋯ :
                                NatTrans (R ⋙ B' ⋙ R₃) (R ⋙ R'' ⋙ B₃) } ≫
                              (R.associator R'' B₃).inv)).natTrans.app
                (T.obj X),
            naturality := ⋯ } ≫
          (T.associator (R ⋙ R'') B₃).inv ≫
            {
                app := fun (X : C₁) ↦
                  B₃.map
                    ((mk T (L ⋙ L') (R ⋙ R'') B''
                            ((T.associator R R'').inv ≫
                              { app := fun (X : C₁) ↦ R''.map (w₁.natTrans.app X), naturality := ⋯ :
                                  NatTrans ((T ⋙ R) ⋙ R'') ((L ⋙ B) ⋙ R'') } ≫
                                (L.associator B R'').hom ≫
                                  { app := fun (X : C₁) ↦ w₃.natTrans.app (L.obj X), naturality := ⋯ :
                                      NatTrans (L ⋙ B ⋙ R'') (L ⋙ L' ⋙ B'') } ≫
                                    (L.associator L' B'').inv)).natTrans.app
                      X),
                naturality := ⋯ : NatTrans ((T ⋙ R ⋙ R'') ⋙ B₃) (((L ⋙ L') ⋙ B'') ⋙ B₃) } ≫
              ((L ⋙ L').associator B'' B₃).hom)
have h : ∀ (c : C₁),
  (mk (T ⋙ T') (L ⋙ L') (R' ⋙ R₃) (B'' ⋙ B₃)
            (((T ⋙ T').associator R' R₃).inv ≫
              {
                  app := fun (X : C₁) ↦
                    R₃.map
                      ((mk (T ⋙ T') L R' (B ⋙ B')
                              ((T.associator T' R').hom ≫
                                { app := fun (X : C₁) ↦ w₂.natTrans.app (T.obj X), naturality := sorry :
                                    NatTrans (T ⋙ T' ⋙ R') (T ⋙ R ⋙ B') } ≫
                                  (T.associator R B').inv ≫
                                    { app := fun (X : C₁) ↦ B'.map (w₁.natTrans.app X), naturality := sorry :
                                        NatTrans ((T ⋙ R) ⋙ B') ((L ⋙ B) ⋙ B') } ≫
                                      (L.associator B B').hom)).natTrans.app
                        X),
                  naturality := sorry : NatTrans (((T ⋙ T') ⋙ R') ⋙ R₃) ((L ⋙ B ⋙ B') ⋙ R₃) } ≫
                (L.associator (B ⋙ B') R₃).hom ≫
                  {
                      app := fun (X : C₁) ↦
                        (mk (B ⋙ B') L' R₃ (B'' ⋙ B₃)
                                ((B.associator B' R₃).hom ≫
                                  { app := fun (X : C₃) ↦ w₄.natTrans.app (B.obj X), naturality := sorry :
                                      NatTrans (B ⋙ B' ⋙ R₃) (B ⋙ R'' ⋙ B₃) } ≫
                                    (B.associator R'' B₃).inv ≫
                                      { app := fun (X : C₃) ↦ B₃.map (w₃.natTrans.app X), naturality := sorry :
                                          NatTrans ((B ⋙ R'') ⋙ B₃) ((L' ⋙ B'') ⋙ B₃) } ≫
                                        (L'.associator B'' B₃).hom)).natTrans.app
                          (L.obj X),
                      naturality := sorry : NatTrans (L ⋙ (B ⋙ B') ⋙ R₃) (L ⋙ L' ⋙ B'' ⋙ B₃) } ≫
                    (L.associator L' (B'' ⋙ B₃)).inv)).natTrans.app
      c =
    (mk (T ⋙ T') (L ⋙ L') (R' ⋙ R₃) (B'' ⋙ B₃)
            ((T.associator T' (R' ⋙ R₃)).hom ≫
              {
                  app := fun (X : C₁) ↦
                    (mk T' (R ⋙ R'') (R' ⋙ R₃) B₃
                            ((T'.associator R' R₃).inv ≫
                              { app := fun (X : C₂) ↦ R₃.map (w₂.natTrans.app X), naturality := sorry } ≫
                                (R.associator B' R₃).hom ≫
                                  { app := fun (X : C₂) ↦ w₄.natTrans.app (R.obj X), naturality := sorry :
                                      NatTrans (R ⋙ B' ⋙ R₃) (R ⋙ R'' ⋙ B₃) } ≫
                                    (R.associator R'' B₃).inv)).natTrans.app
                      (T.obj X),
                  naturality := sorry } ≫
                (T.associator (R ⋙ R'') B₃).inv ≫
                  {
                      app := fun (X : C₁) ↦
                        B₃.map
                          ((mk T (L ⋙ L') (R ⋙ R'') B''
                                  ((T.associator R R'').inv ≫
                                    { app := fun (X : C₁) ↦ R''.map (w₁.natTrans.app X), naturality := sorry :
                                        NatTrans ((T ⋙ R) ⋙ R'') ((L ⋙ B) ⋙ R'') } ≫
                                      (L.associator B R'').hom ≫
                                        { app := fun (X : C₁) ↦ w₃.natTrans.app (L.obj X), naturality := sorry :
                                            NatTrans (L ⋙ B ⋙ R'') (L ⋙ L' ⋙ B'') } ≫
                                          (L.associator L' B'').inv)).natTrans.app
                            X),
                      naturality := sorry : NatTrans ((T ⋙ R ⋙ R'') ⋙ B₃) (((L ⋙ L') ⋙ B'') ⋙ B₃) } ≫
                    ((L ⋙ L').associator B'' B₃).hom)).natTrans.app
      c
Tactic: ext c