-- Mathlib/CategoryTheory/Adjunction/Basic.lean
@[ext]
lemma ext {F : C ⥤ D} {G : D ⥤ C} {adj adj' : F ⊣ G}
    (h : adj.unit = adj'.unit) : adj = adj'

Proof state:
case w.h.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj.counit.app X) = (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj'.counit.app X)

Tactic:
rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
  Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]

Result:
no goals

Proof state:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj' : F ⊣ G
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit =
    adj'.unit
h' :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit =
    adj'.counit
⊢ { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ } =
    adj'

Tactic:
cases adj'

Result:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
unit✝¹ : 𝟭 C ⟶ F ⋙ G
counit✝¹ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝¹ : ∀ (X : C), F.map (unit✝¹.app X) ≫ counit✝¹.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝¹ : ∀ (Y : D), unit✝¹.app (G.obj Y) ≫ G.map (counit✝¹.app Y) = 𝟙 (G.obj Y)
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.unit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit
h' :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.counit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit
⊢ { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
      right_triangle_components := right_triangle_components✝¹ } =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ }

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
⊢ adj = adj'

Tactic:
suffices h' : adj.counit = adj'.counit by cases adj; cases adj'; aesop

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
⊢ adj.counit = adj'.counit

Proof state:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
unit✝¹ : 𝟭 C ⟶ F ⋙ G
counit✝¹ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝¹ : ∀ (X : C), F.map (unit✝¹.app X) ≫ counit✝¹.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝¹ : ∀ (Y : D), unit✝¹.app (G.obj Y) ≫ G.map (counit✝¹.app Y) = 𝟙 (G.obj Y)
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.unit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit
h' :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.counit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit
⊢ { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
      right_triangle_components := right_triangle_components✝¹ } =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ }

Tactic:
aesop

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
h' : adj.counit = adj'.counit
⊢ adj = adj'

Tactic:
cases adj

Result:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj' : F ⊣ G
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit =
    adj'.unit
h' :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit =
    adj'.counit
⊢ { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ } =
    adj'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
⊢ adj.counit = adj'.counit

Tactic:
ext X

Result:
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ adj.counit.app X = adj'.counit.app X

Proof state:
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ adj.counit.app X = adj'.counit.app X

Tactic:
apply (adj.homEquiv _ _).injective

Result:
case w.h.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj.counit.app X) = (adj.homEquiv (G.obj X) ((𝟭 D).obj X)) (adj'.counit.app X)