Module: Mathlib.CategoryTheory.Functor.TwoSquare

Goal state before:
pp: 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₃).inv ≫
              {
                  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₃).hom ≫
                  {
                      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₃)).inv)).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₃).inv ≫
                              { app := fun X ↦ R₃.map (w₂.natTrans.app X), naturality := ⋯ } ≫
                                (R.associator B' R₃).hom ≫
                                  { app := fun X ↦ w₄.natTrans.app (R.obj X), naturality := ⋯ } ≫
                                    (R.associator R'' B₃).inv)).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'').inv ≫
                                    { app := fun X ↦ R''.map (w₁.natTrans.app X), naturality := ⋯ } ≫
                                      (L.associator B R'').hom ≫
                                        { app := fun X ↦ w₃.natTrans.app (L.obj X), naturality := ⋯ } ≫
                                          (L.associator L' B'').inv)).natTrans.app
                            X),
                      naturality := ⋯ } ≫
                    ((L ⋙ L').associator B'' B₃).hom)).natTrans.app
      c

Tactic:
simp only [comp_obj, NatTrans.comp_app, associator_hom_app, associator_inv_app, comp_id, id_comp,
    map_comp, assoc]

Goal state after:
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₁
⊢ R₃.map (w₂.natTrans.app (T.obj c)) ≫
      R₃.map (B'.map (w₁.natTrans.app c)) ≫ w₄.natTrans.app (B.obj (L.obj c)) ≫ B₃.map (w₃.natTrans.app (L.obj c)) =
    R₃.map (w₂.natTrans.app (T.obj c)) ≫
      w₄.natTrans.app (R.obj (T.obj c)) ≫ B₃.map (R''.map (w₁.natTrans.app c)) ≫ B₃.map (w₃.natTrans.app (L.obj c))