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

Tactic:
simp only [comp_id, map_comp, id_comp, assoc]

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

Tactic:
simp only [comp_obj, Functor.comp_map, map_comp, assoc]

Result:
no goals