case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x✝ : D
⊢ (whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit).app x✝ = adj1.counit.app x✝
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
⊢ whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit
ext
no goals
case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x✝ : D
⊢ (whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit).app x✝ = adj1.counit.app x✝
simp