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
⊢ adj1.unit.app x ≫ G.map ((leftAdjointUniq adj1 adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G).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
⊢ adj1.unit.app x ≫ G.map ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x
rw [← unit_leftAdjointUniq_hom adj1 adj2]
no goals
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
⊢ adj1.unit.app x ≫ G.map ((leftAdjointUniq adj1 adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G).app x
rfl