case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ (whiskerLeft G adj.unit ≫ whiskerRight adj.counit G).app x✝ = (𝟙 (G ⋙ 𝟭 C)).app x✝
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
⊢ whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 (G ⋙ 𝟭 C)
ext
case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ adj.unit.app (G.obj x✝) ≫ G.map (adj.counit.app x✝) = 𝟙 (G.obj x✝)
case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ (whiskerLeft G adj.unit ≫ whiskerRight adj.counit G).app x✝ = (𝟙 (G ⋙ 𝟭 C)).app x✝
dsimp
case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ adj.counit.app x✝ = F.map (𝟙 (G.obj x✝)) ≫ adj.counit.app x✝
case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ adj.unit.app (G.obj x✝) ≫ G.map (adj.counit.app x✝) = 𝟙 (G.obj x✝)
erw [← adj.homEquiv_unit, ← Equiv.eq_symm_apply, adj.homEquiv_counit]
no goals
case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ adj.counit.app x✝ = F.map (𝟙 (G.obj x✝)) ≫ adj.counit.app x✝
simp