-- 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₃
⊢ (w₁ ≫ₕ w₂) ≫ᵥ w₃ ≫ₕ w₄ = (w₁ ≫ᵥ w₃) ≫ₕ w₂ ≫ᵥ w₄
have unfold : 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) =
  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)
Tactic: unfold hComp vComp whiskerLeft whiskerRight