-- 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:
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
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      (R₂.map
            (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c)))) ≫
              R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c)) ≫ H.map (adj₁.counit.app (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c)))

Tactic:
rw [R₂.map_comp, L₄.map_comp, R₄.map_comp, R₂.map_comp]

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
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      ((R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
              R₂.map (R₄.map (L₄.map (H.map (adj₁.counit.app (R₃.obj c)))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c)))

Proof state:
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
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      ((R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
              R₂.map (R₄.map (L₄.map (H.map (adj₁.counit.app (R₃.obj c)))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c)))

Tactic:
slice_rhs 4 5 =>
  rw [← R₂.map_comp, ← R₄.map_comp, ← Functor.comp_map _ L₄ , β.naturality]

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
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.app (L₁.obj (R₁.obj (R₃.obj c))) ≫ (L₃ ⋙ K).map (adj₁.counit.app (R₃.obj c)))) ≫
            R₂.map (R₄.map (K.map (adj₃.counit.app c)))