-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem mateEquiv_hcomp (α : TwoSquare G L₁ L₂ H) (β : TwoSquare H L₃ L₄ K) :
    (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (α ≫ᵥ β) =
      (mateEquiv adj₃ adj₄ β) ≫ₕ (mateEquiv adj₁ adj₂ α)

Proof state:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G : A ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
⊢ {
        toFun := fun α =>
          TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
            (whiskerLeft ((R₃ ⋙ R₁) ⋙ G)
                (mk'
                    { homEquiv := fun x x_1 => (adj₄.homEquiv (L₂.obj x) x_1).trans (adj₂.homEquiv x (R₄.obj x_1)),
                      unit :=
                        adj₂.unit ≫
                          whiskerRight (L₂.rightUnitor.inv ≫ whiskerLeft L₂ adj₄.unit ≫ (L₂.associator L₄ R₄).inv) R₂ ≫
                            ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                      counit :=
                        ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                          whiskerRight ((R₄.associator R₂ L₂).hom ≫ whiskerLeft R₄ adj₂.counit ≫ R₄.rightUnitor.hom)
                              L₄ ≫
                            adj₄.counit,
                      homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).unit ≫
              whiskerRight (whiskerLeft (R₃ ⋙ R₁) α.natTrans) (R₄ ⋙ R₂) ≫
                whiskerRight
                  (mk'
                      { homEquiv := fun x x_1 => (adj₃.homEquiv (L₁.obj x) x_1).trans (adj₁.homEquiv x (R₃.obj x_1)),
                        unit :=
                          adj₁.unit ≫
                            whiskerRight (L₁.rightUnitor.inv ≫ whiskerLeft L₁ adj₃.unit ≫ (L₁.associator L₃ R₃).inv)
                                R₁ ≫
                              ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                        counit :=
                          ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                            whiskerRight ((R₃.associator R₁ L₁).hom ≫ whiskerLeft R₃ adj₁.counit ≫ R₃.rightUnitor.hom)
                                L₃ ≫
                              adj₃.counit,
                        homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).counit
                  (K ⋙ R₄ ⋙ R₂)),
        invFun := fun β =>
          TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
            (whiskerRight
                (mk'
                    { homEquiv := fun x x_1 => (adj₃.homEquiv (L₁.obj x) x_1).trans (adj₁.homEquiv x (R₃.obj x_1)),
                      unit :=
                        adj₁.unit ≫
                          whiskerRight (L₁.rightUnitor.inv ≫ whiskerLeft L₁ adj₃.unit ≫ (L₁.associator L₃ R₃).inv) R₁ ≫
                            ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                      counit :=
                        ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                          whiskerRight ((R₃.associator R₁ L₁).hom ≫ whiskerLeft R₃ adj₁.counit ≫ R₃.rightUnitor.hom)
                              L₃ ≫
                            adj₃.counit,
                      homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).unit
                (G ⋙ L₂ ⋙ L₄) ≫
              whiskerRight (whiskerLeft (L₁ ⋙ L₃) β.natTrans) (L₂ ⋙ L₄) ≫
                whiskerLeft ((L₁ ⋙ L₃) ⋙ K)
                  (mk'
                      { homEquiv := fun x x_1 => (adj₄.homEquiv (L₂.obj x) x_1).trans (adj₂.homEquiv x (R₄.obj x_1)),
                        unit :=
                          adj₂.unit ≫
                            whiskerRight (L₂.rightUnitor.inv ≫ whiskerLeft L₂ adj₄.unit ≫ (L₂.associator L₄ R₄).inv)
                                R₂ ≫
                              ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                        counit :=
                          ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                            whiskerRight ((R₄.associator R₂ L₂).hom ≫ whiskerLeft R₄ adj₂.counit ≫ R₄.rightUnitor.hom)
                                L₄ ≫
                              adj₄.counit,
                        homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).counit),
        left_inv := ⋯, right_inv := ⋯ }
      (TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
        ((G.associator L₂ L₄).hom ≫
          whiskerRight α.natTrans L₄ ≫
            (L₁.associator H L₄).inv ≫ whiskerLeft L₁ β.natTrans ≫ (L₁.associator L₃ K).hom)) =
    TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
      ((R₃.associator R₁ G).hom ≫
        whiskerLeft R₃
            ({
                  toFun := fun α =>
                    TwoSquare.mk R₁ H G R₂
                      (whiskerLeft (R₁ ⋙ G) adj₂.unit ≫
                        whiskerRight (whiskerLeft R₁ α.natTrans) R₂ ≫ whiskerRight adj₁.counit (H ⋙ R₂)),
                  invFun := fun β =>
                    TwoSquare.mk G L₁ L₂ H
                      (whiskerRight adj₁.unit (G ⋙ L₂) ≫
                        whiskerRight (whiskerLeft L₁ β.natTrans) L₂ ≫ whiskerLeft (L₁ ⋙ H) adj₂.counit),
                  left_inv := ⋯, right_inv := ⋯ }
                α).natTrans ≫
          (R₃.associator H R₂).inv ≫
            whiskerRight
                ({
                      toFun := fun α =>
                        TwoSquare.mk R₃ K H R₄
                          (whiskerLeft (R₃ ⋙ H) adj₄.unit ≫
                            whiskerRight (whiskerLeft R₃ α.natTrans) R₄ ≫ whiskerRight adj₃.counit (K ⋙ R₄)),
                      invFun := fun β =>
                        TwoSquare.mk H L₃ L₄ K
                          (whiskerRight adj₃.unit (H ⋙ L₄) ≫
                            whiskerRight (whiskerLeft L₃ β.natTrans) L₄ ≫ whiskerLeft (L₃ ⋙ K) adj₄.counit),
                      left_inv := ⋯, right_inv := ⋯ }
                    β).natTrans
                R₂ ≫
              (K.associator R₄ R₂).hom)

Tactic:
ext c

Result:
case h
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G : A ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ ({
              toFun := fun α =>
                TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
                  (whiskerLeft ((R₃ ⋙ R₁) ⋙ G)
                      (mk'
                          {
                            homEquiv := fun x x_1 =>
                              (adj₄.homEquiv (L₂.obj x) x_1).trans (adj₂.homEquiv x (R₄.obj x_1)),
                            unit :=
                              adj₂.unit ≫
                                whiskerRight (L₂.rightUnitor.inv ≫ whiskerLeft L₂ adj₄.unit ≫ (L₂.associator L₄ R₄).inv)
                                    R₂ ≫
                                  ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                            counit :=
                              ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                                whiskerRight
                                    ((R₄.associator R₂ L₂).hom ≫ whiskerLeft R₄ adj₂.counit ≫ R₄.rightUnitor.hom) L₄ ≫
                                  adj₄.counit,
                            homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).unit ≫
                    whiskerRight (whiskerLeft (R₃ ⋙ R₁) α.natTrans) (R₄ ⋙ R₂) ≫
                      whiskerRight
                        (mk'
                            {
                              homEquiv := fun x x_1 =>
                                (adj₃.homEquiv (L₁.obj x) x_1).trans (adj₁.homEquiv x (R₃.obj x_1)),
                              unit :=
                                adj₁.unit ≫
                                  whiskerRight
                                      (L₁.rightUnitor.inv ≫ whiskerLeft L₁ adj₃.unit ≫ (L₁.associator L₃ R₃).inv) R₁ ≫
                                    ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                              counit :=
                                ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                                  whiskerRight
                                      ((R₃.associator R₁ L₁).hom ≫ whiskerLeft R₃ adj₁.counit ≫ R₃.rightUnitor.hom) L₃ ≫
                                    adj₃.counit,
                              homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).counit
                        (K ⋙ R₄ ⋙ R₂)),
              invFun := fun β =>
                TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
                  (whiskerRight
                      (mk'
                          {
                            homEquiv := fun x x_1 =>
                              (adj₃.homEquiv (L₁.obj x) x_1).trans (adj₁.homEquiv x (R₃.obj x_1)),
                            unit :=
                              adj₁.unit ≫
                                whiskerRight (L₁.rightUnitor.inv ≫ whiskerLeft L₁ adj₃.unit ≫ (L₁.associator L₃ R₃).inv)
                                    R₁ ≫
                                  ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                            counit :=
                              ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                                whiskerRight
                                    ((R₃.associator R₁ L₁).hom ≫ whiskerLeft R₃ adj₁.counit ≫ R₃.rightUnitor.hom) L₃ ≫
                                  adj₃.counit,
                            homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).unit
                      (G ⋙ L₂ ⋙ L₄) ≫
                    whiskerRight (whiskerLeft (L₁ ⋙ L₃) β.natTrans) (L₂ ⋙ L₄) ≫
                      whiskerLeft ((L₁ ⋙ L₃) ⋙ K)
                        (mk'
                            {
                              homEquiv := fun x x_1 =>
                                (adj₄.homEquiv (L₂.obj x) x_1).trans (adj₂.homEquiv x (R₄.obj x_1)),
                              unit :=
                                adj₂.unit ≫
                                  whiskerRight
                                      (L₂.rightUnitor.inv ≫ whiskerLeft L₂ adj₄.unit ≫ (L₂.associator L₄ R₄).inv) R₂ ≫
                                    ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                              counit :=
                                ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                                  whiskerRight
                                      ((R₄.associator R₂ L₂).hom ≫ whiskerLeft R₄ adj₂.counit ≫ R₄.rightUnitor.hom) L₄ ≫
                                    adj₄.counit,
                              homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).counit),
              left_inv := ⋯, right_inv := ⋯ }
            (TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
              ((G.associator L₂ L₄).hom ≫
                whiskerRight α.natTrans L₄ ≫
                  (L₁.associator H L₄).inv ≫ whiskerLeft L₁ β.natTrans ≫ (L₁.associator L₃ K).hom))).natTrans.app
      c =
    (TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
            ((R₃.associator R₁ G).hom ≫
              whiskerLeft R₃
                  ({
                        toFun := fun α =>
                          TwoSquare.mk R₁ H G R₂
                            (whiskerLeft (R₁ ⋙ G) adj₂.unit ≫
                              whiskerRight (whiskerLeft R₁ α.natTrans) R₂ ≫ whiskerRight adj₁.counit (H ⋙ R₂)),
                        invFun := fun β =>
                          TwoSquare.mk G L₁ L₂ H
                            (whiskerRight adj₁.unit (G ⋙ L₂) ≫
                              whiskerRight (whiskerLeft L₁ β.natTrans) L₂ ≫ whiskerLeft (L₁ ⋙ H) adj₂.counit),
                        left_inv := ⋯, right_inv := ⋯ }
                      α).natTrans ≫
                (R₃.associator H R₂).inv ≫
                  whiskerRight
                      ({
                            toFun := fun α =>
                              TwoSquare.mk R₃ K H R₄
                                (whiskerLeft (R₃ ⋙ H) adj₄.unit ≫
                                  whiskerRight (whiskerLeft R₃ α.natTrans) R₄ ≫ whiskerRight adj₃.counit (K ⋙ R₄)),
                            invFun := fun β =>
                              TwoSquare.mk H L₃ L₄ K
                                (whiskerRight adj₃.unit (H ⋙ L₄) ≫
                                  whiskerRight (whiskerLeft L₃ β.natTrans) L₄ ≫ whiskerLeft (L₃ ⋙ K) adj₄.counit),
                            left_inv := ⋯, right_inv := ⋯ }
                          β).natTrans
                      R₂ ≫
                    (K.associator R₄ R₂).hom)).natTrans.app
      c