case 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 : C
⊢ ↑(homEquiv adj1 x (F'.obj x)).symm (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x)) =
    ↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.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
x : C
⊢ ↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x
apply (adj1.homEquiv _ _).symm.injective
case 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 : C
⊢ (↑(homEquiv adj1 x (F'.obj x)).symm (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x))).op =
    (↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.app x)).op
case 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 : C
⊢ ↑(homEquiv adj1 x (F'.obj x)).symm (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x)) =
    ↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.app x)
apply Quiver.Hom.op_inj
case a.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 : C
⊢ coyoneda.map
      (↑(homEquiv adj1 x (F'.obj x)).symm (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x))).op =
    coyoneda.map (↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.app x)).op
case 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 : C
⊢ (↑(homEquiv adj1 x (F'.obj x)).symm (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x))).op =
    (↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.app x)).op
apply coyoneda.map_injective
case a.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 : C
x✝ : D
a✝ : (coyoneda.obj (F'.obj x).op).obj x✝
⊢ (coyoneda.map
          (↑(homEquiv adj1 x (F'.obj x)).symm
              (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x))).op).app
      x✝ a✝ =
    (coyoneda.map (↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.app x)).op).app x✝ a✝
case a.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 : C
⊢ coyoneda.map
      (↑(homEquiv adj1 x (F'.obj x)).symm (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x))).op =
    coyoneda.map (↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.app x)).op
ext
case a.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 : C
x✝ : D
a✝ : (coyoneda.obj (F'.obj x).op).obj x✝
⊢ (coyoneda.map
          (↑(homEquiv adj1 x (F'.obj x)).symm
              (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x))).op).app
      x✝ a✝ =
    (coyoneda.map (↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.app x)).op).app x✝ a✝
case a.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 : C
x✝ : D
a✝ : (coyoneda.obj (F'.obj x).op).obj x✝
⊢ (coyoneda.map
          (↑(homEquiv adj1 x (F'.obj x)).symm
              (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x))).op).app
      x✝ a✝ =
    (coyoneda.map (↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.app x)).op).app x✝ a✝
funext
no goals
case a.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 : C
x✝ : D
a✝ : (coyoneda.obj (F'.obj x).op).obj x✝
⊢ (coyoneda.map
          (↑(homEquiv adj1 x (F'.obj x)).symm
              (↑(homEquiv adj1 x (F'.obj x)) ((leftAdjointUniq adj1 adj2).hom.app x))).op).app
      x✝ a✝ =
    (coyoneda.map (↑(homEquiv adj1 x (F'.obj x)).symm (adj2.unit.app x)).op).app x✝ a✝
simp [leftAdjointUniq, leftAdjointsCoyonedaEquiv]