case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝ : C
⊢ (leftAdjointUniq adj1 adj1).hom.app x✝ = (𝟙 F).app x✝
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (leftAdjointUniq adj1 adj1).hom = 𝟙 F
ext
case w.h.a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝ : C
⊢ ((leftAdjointUniq adj1 adj1).hom.app x✝).op = ((𝟙 F).app x✝).op
case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝ : C
⊢ (leftAdjointUniq adj1 adj1).hom.app x✝ = (𝟙 F).app x✝
apply Quiver.Hom.op_inj
case w.h.a.a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝ : C
⊢ coyoneda.map ((leftAdjointUniq adj1 adj1).hom.app x✝).op = coyoneda.map ((𝟙 F).app x✝).op
case w.h.a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝ : C
⊢ ((leftAdjointUniq adj1 adj1).hom.app x✝).op = ((𝟙 F).app x✝).op
apply coyoneda.map_injective
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝¹ : C
x✝ : D
a✝ : (coyoneda.obj (F.obj x✝¹).op).obj x✝
⊢ (coyoneda.map ((leftAdjointUniq adj1 adj1).hom.app x✝¹).op).app x✝ a✝ = (coyoneda.map ((𝟙 F).app x✝¹).op).app x✝ a✝
case w.h.a.a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝ : C
⊢ coyoneda.map ((leftAdjointUniq adj1 adj1).hom.app x✝).op = coyoneda.map ((𝟙 F).app x✝).op
ext
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝¹ : C
x✝ : D
a✝ : (coyoneda.obj (F.obj x✝¹).op).obj x✝
⊢ (coyoneda.map ((leftAdjointUniq adj1 adj1).hom.app x✝¹).op).app x✝ a✝ = (coyoneda.map ((𝟙 F).app x✝¹).op).app x✝ a✝
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝¹ : C
x✝ : D
a✝ : (coyoneda.obj (F.obj x✝¹).op).obj x✝
⊢ (coyoneda.map ((leftAdjointUniq adj1 adj1).hom.app x✝¹).op).app x✝ a✝ = (coyoneda.map ((𝟙 F).app x✝¹).op).app x✝ a✝
funext
no goals
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝¹ : C
x✝ : D
a✝ : (coyoneda.obj (F.obj x✝¹).op).obj x✝
⊢ (coyoneda.map ((leftAdjointUniq adj1 adj1).hom.app x✝¹).op).app x✝ a✝ = (coyoneda.map ((𝟙 F).app x✝¹).op).app x✝ a✝
simp [leftAdjointsCoyonedaEquiv, leftAdjointUniq]