case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x = adj1.counit.app x
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit
ext x
case w.h.a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ ((whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x).op = (adj1.counit.app x).op
case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x = adj1.counit.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 F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ coyoneda.map ((whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x).op =
    coyoneda.map (adj1.counit.app x).op
case w.h.a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ ((whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x).op = (adj1.counit.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 F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x x✝ : D
a✝ : (coyoneda.obj ((𝟭 D).obj x).op).obj x✝
⊢ (coyoneda.map ((whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x).op).app x✝ a✝ =
    (coyoneda.map (adj1.counit.app x).op).app x✝ a✝
case w.h.a.a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ coyoneda.map ((whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x).op =
    coyoneda.map (adj1.counit.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 F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x x✝ : D
a✝ : (coyoneda.obj ((𝟭 D).obj x).op).obj x✝
⊢ (coyoneda.map ((whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x).op).app x✝ a✝ =
    (coyoneda.map (adj1.counit.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 F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x x✝ : D
a✝ : (coyoneda.obj ((𝟭 D).obj x).op).obj x✝
⊢ (coyoneda.map ((whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x).op).app x✝ a✝ =
    (coyoneda.map (adj1.counit.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 F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x x✝ : D
a✝ : (coyoneda.obj ((𝟭 D).obj x).op).obj x✝
⊢ (coyoneda.map ((whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit).app x).op).app x✝ a✝ =
    (coyoneda.map (adj1.counit.app x).op).app x✝ a✝
simp [leftAdjointUniq, leftAdjointsCoyonedaEquiv]