diff --git a/Mathlib.lean b/Mathlib.lean
index 9157b4b7b4483..a541c84f0abdc 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1172,6 +1172,7 @@ import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Adjunction.Over
 import Mathlib.CategoryTheory.Adjunction.Reflective
 import Mathlib.CategoryTheory.Adjunction.Restrict
+import Mathlib.CategoryTheory.Adjunction.Unique
 import Mathlib.CategoryTheory.Adjunction.Whiskering
 import Mathlib.CategoryTheory.Balanced
 import Mathlib.CategoryTheory.Bicategory.Adjunction
diff --git a/Mathlib/CategoryTheory/Adjunction/Opposites.lean b/Mathlib/CategoryTheory/Adjunction/Opposites.lean
index 7fd21fa04b633..252772733c9c6 100644
--- a/Mathlib/CategoryTheory/Adjunction/Opposites.lean
+++ b/Mathlib/CategoryTheory/Adjunction/Opposites.lean
@@ -14,7 +14,6 @@ import Mathlib.CategoryTheory.Opposites
 
 This file contains constructions to relate adjunctions of functors to adjunctions of their
 opposites.
-These constructions are used to show uniqueness of adjoints (up to natural isomorphism).
 
 ## Tags
 adjunction, opposite, uniqueness
@@ -128,213 +127,27 @@ def leftAdjointsCoyonedaEquiv {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (a
       ((adj1.homEquiv X.unop Y).trans (adj2.homEquiv X.unop Y).symm).toIso
 #align category_theory.adjunction.left_adjoints_coyoneda_equiv CategoryTheory.Adjunction.leftAdjointsCoyonedaEquiv
 
-/-- If `F` and `F'` are both left adjoint to `G`, then they are naturally isomorphic. -/
-def leftAdjointUniq {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
-    F ≅ F' :=
-  NatIso.removeOp (Coyoneda.preimageNatIso (leftAdjointsCoyonedaEquiv adj2 adj1))
-#align category_theory.adjunction.left_adjoint_uniq CategoryTheory.Adjunction.leftAdjointUniq
-
--- Porting note (#10618): removed simp as simp can prove this
-theorem homEquiv_leftAdjointUniq_hom_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
-    (x : C) : adj1.homEquiv _ _ ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x := by
-  apply (adj1.homEquiv _ _).symm.injective
-  apply Quiver.Hom.op_inj
-  apply coyoneda.map_injective
-  --swap; infer_instance
-  ext
-  simp [leftAdjointUniq, leftAdjointsCoyonedaEquiv]
-#align category_theory.adjunction.hom_equiv_left_adjoint_uniq_hom_app CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app
-
-@[reassoc (attr := simp)]
-theorem unit_leftAdjointUniq_hom {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
-    adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G = adj2.unit := by
-  ext x
-  rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]
-  simp [← G.map_comp]
-#align category_theory.adjunction.unit_left_adjoint_uniq_hom CategoryTheory.Adjunction.unit_leftAdjointUniq_hom
-
-@[reassoc (attr := simp)]
-theorem unit_leftAdjointUniq_hom_app {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 :=
-  by rw [← unit_leftAdjointUniq_hom adj1 adj2]; rfl
-#align category_theory.adjunction.unit_left_adjoint_uniq_hom_app CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app
-
-@[reassoc (attr := simp)]
-theorem leftAdjointUniq_hom_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
-    whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit := by
-  ext x
-  apply Quiver.Hom.op_inj
-  apply coyoneda.map_injective
-  ext
-  simp [leftAdjointUniq, leftAdjointsCoyonedaEquiv]
-#align category_theory.adjunction.left_adjoint_uniq_hom_counit CategoryTheory.Adjunction.leftAdjointUniq_hom_counit
-
-@[reassoc (attr := simp)]
-theorem leftAdjointUniq_hom_app_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
-    (x : D) :
-    (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x := by
-  rw [← leftAdjointUniq_hom_counit adj1 adj2]
-  rfl
-#align category_theory.adjunction.left_adjoint_uniq_hom_app_counit CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit
-
-@[simp]
-theorem leftAdjointUniq_inv_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
-    (leftAdjointUniq adj1 adj2).inv.app x = (leftAdjointUniq adj2 adj1).hom.app x :=
-  rfl
-#align category_theory.adjunction.left_adjoint_uniq_inv_app CategoryTheory.Adjunction.leftAdjointUniq_inv_app
-
-@[reassoc (attr := simp)]
-theorem leftAdjointUniq_trans {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
-    (adj3 : F'' ⊣ G) :
-    (leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom =
-      (leftAdjointUniq adj1 adj3).hom := by
-  ext
-  apply Quiver.Hom.op_inj
-  apply coyoneda.map_injective
-  ext
-  simp [leftAdjointsCoyonedaEquiv, leftAdjointUniq]
-#align category_theory.adjunction.left_adjoint_uniq_trans CategoryTheory.Adjunction.leftAdjointUniq_trans
-
-@[reassoc (attr := simp)]
-theorem leftAdjointUniq_trans_app {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
-    (adj3 : F'' ⊣ G) (x : C) :
-    (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x =
-      (leftAdjointUniq adj1 adj3).hom.app x := by
-  rw [← leftAdjointUniq_trans adj1 adj2 adj3]
-  rfl
-#align category_theory.adjunction.left_adjoint_uniq_trans_app CategoryTheory.Adjunction.leftAdjointUniq_trans_app
-
-@[simp]
-theorem leftAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
-    (leftAdjointUniq adj1 adj1).hom = 𝟙 _ := by
-  ext
-  apply Quiver.Hom.op_inj
-  apply coyoneda.map_injective
-  ext
-  simp [leftAdjointsCoyonedaEquiv, leftAdjointUniq]
-#align category_theory.adjunction.left_adjoint_uniq_refl CategoryTheory.Adjunction.leftAdjointUniq_refl
-
-/-- If `G` and `G'` are both right adjoint to `F`, then they are naturally isomorphic. -/
-def rightAdjointUniq {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
-    G ≅ G' :=
-  NatIso.removeOp (leftAdjointUniq (opAdjointOpOfAdjoint _ F adj2) (opAdjointOpOfAdjoint _ _ adj1))
-#align category_theory.adjunction.right_adjoint_uniq CategoryTheory.Adjunction.rightAdjointUniq
-
--- Porting note (#10618): simp can prove this
-theorem homEquiv_symm_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G)
-    (adj2 : F ⊣ G') (x : D) :
-    (adj2.homEquiv _ _).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x := by
-  apply Quiver.Hom.op_inj
-  convert homEquiv_leftAdjointUniq_hom_app (opAdjointOpOfAdjoint _ F adj2)
-    (opAdjointOpOfAdjoint _ _ adj1) (Opposite.op x)
-  -- Porting note: was `simpa`
-  simp only [opAdjointOpOfAdjoint, Functor.op_obj, Opposite.unop_op, mkOfHomEquiv_unit_app,
-    Equiv.trans_apply, homEquiv_counit, Functor.id_obj]
-  -- Porting note: Yet another `erw`...
-  -- https://github.com/leanprover-community/mathlib4/issues/5164
-  erw [F.map_id]
-  rw [Category.id_comp]
-  rfl
-#align category_theory.adjunction.hom_equiv_symm_right_adjoint_uniq_hom_app CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app
-
-@[reassoc (attr := simp)]
-theorem unit_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
-    (x : C) : adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x) =
-      adj2.unit.app x := by
-  apply Quiver.Hom.op_inj
-  convert
-    leftAdjointUniq_hom_app_counit (opAdjointOpOfAdjoint _ _ adj2)
-      (opAdjointOpOfAdjoint _ _ adj1) (Opposite.op x) using 1
-  --all_goals simp
-  all_goals {
-    -- Porting note: Again, something seems wrong here... Some `simp` lemmas are not firing!
-    simp only [Functor.id_obj, Functor.comp_obj, op_comp, Functor.op_obj, Opposite.unop_op,
-      opAdjointOpOfAdjoint, mkOfHomEquiv_counit_app, Equiv.invFun_as_coe, Equiv.symm_trans_apply,
-      Equiv.symm_symm, homEquiv_unit]
-    erw [Functor.map_id]
-    rw [Category.comp_id]
-    rfl }
-#align category_theory.adjunction.unit_right_adjoint_uniq_hom_app CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app
-
-@[reassoc (attr := simp)]
-theorem unit_rightAdjointUniq_hom {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
-    adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom = adj2.unit := by
-  ext x
-  simp
-#align category_theory.adjunction.unit_right_adjoint_uniq_hom CategoryTheory.Adjunction.unit_rightAdjointUniq_hom
-
-@[reassoc (attr := simp)]
-theorem rightAdjointUniq_hom_app_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
-    (x : D) :
-    F.map ((rightAdjointUniq adj1 adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x := by
-  apply Quiver.Hom.op_inj
-  convert
-    unit_leftAdjointUniq_hom_app (opAdjointOpOfAdjoint _ _ adj2)
-      (opAdjointOpOfAdjoint _ _ adj1) (Opposite.op x) using 1
-  · simp only [Functor.id_obj, op_comp, Functor.comp_obj, Functor.op_obj, Opposite.unop_op,
-      opAdjointOpOfAdjoint_unit_app, Functor.op_map]
-    dsimp [opEquiv]
-    simp only [← op_comp]
-    congr 2
-    simp
-  · simp only [Functor.id_obj, opAdjointOpOfAdjoint_unit_app, Opposite.unop_op]
-    erw [Functor.map_id, Category.id_comp]
-    rfl
-#align category_theory.adjunction.right_adjoint_uniq_hom_app_counit CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit
-
-@[reassoc (attr := simp)]
-theorem rightAdjointUniq_hom_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
-    whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit := by
-  ext
-  simp
-#align category_theory.adjunction.right_adjoint_uniq_hom_counit CategoryTheory.Adjunction.rightAdjointUniq_hom_counit
-
-@[simp]
-theorem rightAdjointUniq_inv_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
-    (x : D) : (rightAdjointUniq adj1 adj2).inv.app x = (rightAdjointUniq adj2 adj1).hom.app x :=
-  rfl
-#align category_theory.adjunction.right_adjoint_uniq_inv_app CategoryTheory.Adjunction.rightAdjointUniq_inv_app
-
-@[reassoc (attr := simp)]
-theorem rightAdjointUniq_trans_app {F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
-    (adj3 : F ⊣ G'') (x : D) :
-    (rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x =
-      (rightAdjointUniq adj1 adj3).hom.app x := by
-  apply Quiver.Hom.op_inj
-  dsimp [rightAdjointUniq]
-  simp
-#align category_theory.adjunction.right_adjoint_uniq_trans_app CategoryTheory.Adjunction.rightAdjointUniq_trans_app
-
-@[reassoc (attr := simp)]
-theorem rightAdjointUniq_trans {F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
-    (adj3 : F ⊣ G'') :
-    (rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom =
-      (rightAdjointUniq adj1 adj3).hom := by
-  ext
-  simp
-#align category_theory.adjunction.right_adjoint_uniq_trans CategoryTheory.Adjunction.rightAdjointUniq_trans
+/-- Given two adjunctions, if the right adjoints are naturally isomorphic, then so are the left
+adjoints.
 
-@[simp]
-theorem rightAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
-    (rightAdjointUniq adj1 adj1).hom = 𝟙 _ := by
-  delta rightAdjointUniq
-  simp
-#align category_theory.adjunction.right_adjoint_uniq_refl CategoryTheory.Adjunction.rightAdjointUniq_refl
+Note: it is generally better to use `Adjunction.natIsoEquiv`, see the file `Adjunction.Unique`.
+The reason this definition still exists is that apparently `CategoryTheory.extendAlongYonedaYoneda`
+uses its definitional properties (TODO: figure out a way to avoid this).
+-/
+def natIsoOfRightAdjointNatIso {F F' : C ⥤ D} {G G' : D ⥤ C}
+    (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (r : G ≅ G') : F ≅ F' :=
+  NatIso.removeOp (Coyoneda.preimageNatIso (leftAdjointsCoyonedaEquiv adj2 (adj1.ofNatIsoRight r)))
+#align category_theory.adjunction.nat_iso_of_right_adjoint_nat_iso CategoryTheory.Adjunction.natIsoOfRightAdjointNatIso
 
 /-- Given two adjunctions, if the left adjoints are naturally isomorphic, then so are the right
 adjoints.
+
+Note: it is generally better to use `Adjunction.natIsoEquiv`, see the file `Adjunction.Unique`.
 -/
 def natIsoOfLeftAdjointNatIso {F F' : C ⥤ D} {G G' : D ⥤ C}
     (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (l : F ≅ F') : G ≅ G' :=
-  rightAdjointUniq adj1 (adj2.ofNatIsoLeft l.symm)
+  NatIso.removeOp (natIsoOfRightAdjointNatIso (opAdjointOpOfAdjoint _ F' adj2)
+    (opAdjointOpOfAdjoint _ _ adj1) (NatIso.op l))
 #align category_theory.adjunction.nat_iso_of_left_adjoint_nat_iso CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso
 
-/-- Given two adjunctions, if the right adjoints are naturally isomorphic, then so are the left
-adjoints.
--/
-def natIsoOfRightAdjointNatIso {F F' : C ⥤ D} {G G' : D ⥤ C}
-    (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (r : G ≅ G') : F ≅ F' :=
-  leftAdjointUniq adj1 (adj2.ofNatIsoRight r.symm)
-#align category_theory.adjunction.nat_iso_of_right_adjoint_nat_iso CategoryTheory.Adjunction.natIsoOfRightAdjointNatIso
-
 end CategoryTheory.Adjunction
diff --git a/Mathlib/CategoryTheory/Adjunction/Unique.lean b/Mathlib/CategoryTheory/Adjunction/Unique.lean
new file mode 100644
index 0000000000000..f704023311bd9
--- /dev/null
+++ b/Mathlib/CategoryTheory/Adjunction/Unique.lean
@@ -0,0 +1,254 @@
+/-
+Copyright (c) 2020 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta, Thomas Read, Andrew Yang, Dagur Asgeirsson, Joël Riou
+-/
+import Mathlib.CategoryTheory.Adjunction.Basic
+/-!
+
+# Uniqueness of adjoints
+
+This file shows that adjoints are unique up to natural isomorphism.
+
+## Main results
+* `Adjunction.natTransEquiv` and `Adjunction.natIsoEquiv` If `F ⊣ G` and `F' ⊣ G'` are adjunctions,
+  then there are equivalences `(G ⟶ G') ≃ (F' ⟶ F)` and `(G ≅ G') ≃ (F' ≅ F)`.
+Everything else is deduced from this:
+
+* `Adjunction.leftAdjointUniq` : If `F` and `F'` are both left adjoint to `G`, then they are
+  naturally isomorphic.
+
+* `Adjunction.rightAdjointUniq` : If `G` and `G'` are both right adjoint to `F`, then they are
+  naturally isomorphic.
+-/
+
+open CategoryTheory
+
+variable {C D : Type*} [Category C] [Category D]
+
+namespace CategoryTheory.Adjunction
+
+/--
+If `F ⊣ G` and `F' ⊣ G'` are adjunctions, then giving a natural transformation `G ⟶ G'` is the
+same as giving a natural transformation `F' ⟶ F`.
+-/
+@[simps]
+def natTransEquiv {F F' : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') :
+    (G ⟶ G') ≃ (F' ⟶ F) where
+  toFun f := {
+    app := fun X ↦ F'.map ((adj1.unit ≫ whiskerLeft F f).app X) ≫ adj2.counit.app _
+    naturality := by
+      intro X Y g
+      simp only [← Category.assoc, ← Functor.map_comp]
+      erw [(adj1.unit ≫ (whiskerLeft F f)).naturality]
+      simp
+  }
+  invFun f := {
+    app := fun X ↦ adj2.unit.app (G.obj X) ≫ G'.map (f.app (G.obj X) ≫ adj1.counit.app X)
+    naturality := by
+      intro X Y g
+      erw [← adj2.unit_naturality_assoc]
+      simp only [← Functor.map_comp]
+      simp
+  }
+  left_inv f := by
+    ext X
+    simp only [Functor.comp_obj, NatTrans.comp_app, Functor.id_obj, whiskerLeft_app,
+      Functor.map_comp, Category.assoc, unit_naturality_assoc, right_triangle_components_assoc]
+    erw [← f.naturality (adj1.counit.app X), ← Category.assoc]
+    simp
+  right_inv f := by
+    ext
+    simp
+
+@[simp]
+lemma natTransEquiv_id {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
+    natTransEquiv adj adj (𝟙 _) = 𝟙 _ := by ext; simp
+
+@[simp]
+lemma natTransEquiv_id_symm {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
+    (natTransEquiv adj adj).symm (𝟙 _) = 𝟙 _ := by ext; simp
+
+@[simp]
+lemma natTransEquiv_comp {F F' F'' : C ⥤ D} {G G' G'' : D ⥤ C}
+    (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (adj3 : F'' ⊣ G'') (f : G ⟶ G') (g : G' ⟶ G'') :
+    natTransEquiv adj2 adj3 g ≫ natTransEquiv adj1 adj2 f = natTransEquiv adj1 adj3 (f ≫ g) := by
+  apply (natTransEquiv adj1 adj3).symm.injective
+  ext X
+  simp only [natTransEquiv_symm_apply_app, Functor.comp_obj, NatTrans.comp_app,
+    natTransEquiv_apply_app, Functor.id_obj, whiskerLeft_app, Functor.map_comp, Category.assoc,
+    unit_naturality_assoc, right_triangle_components_assoc, Equiv.symm_apply_apply,
+    ← g.naturality_assoc, ← g.naturality]
+  simp only [← Category.assoc, unit_naturality, Functor.comp_obj, right_triangle_components,
+    Category.comp_id, ← f.naturality, Category.id_comp]
+
+@[simp]
+lemma natTransEquiv_comp_symm {F F' F'' : C ⥤ D} {G G' G'' : D ⥤ C}
+    (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (adj3 : F'' ⊣ G'') (f : F' ⟶ F) (g : F'' ⟶ F') :
+    (natTransEquiv adj1 adj2).symm f ≫ (natTransEquiv adj2 adj3).symm g =
+      (natTransEquiv adj1 adj3).symm (g ≫ f) := by
+  apply (natTransEquiv adj1 adj3).injective
+  ext
+  simp
+
+/--
+If `F ⊣ G` and `F' ⊣ G'` are adjunctions, then giving a natural isomorphism `G ≅ G'` is the
+same as giving a natural transformation `F' ≅ F`.
+-/
+@[simps]
+def natIsoEquiv {F F' : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') :
+    (G ≅ G') ≃ (F' ≅ F) where
+  toFun i := {
+    hom := natTransEquiv adj1 adj2 i.hom
+    inv := natTransEquiv adj2 adj1 i.inv
+  }
+  invFun i := {
+    hom := (natTransEquiv adj1 adj2).symm i.hom
+    inv := (natTransEquiv adj2 adj1).symm i.inv }
+  left_inv i := by simp
+  right_inv i := by simp
+
+/-- If `F` and `F'` are both left adjoint to `G`, then they are naturally isomorphic. -/
+def leftAdjointUniq {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) : F ≅ F' :=
+  (natIsoEquiv adj1 adj2 (Iso.refl _)).symm
+#align category_theory.adjunction.left_adjoint_uniq CategoryTheory.Adjunction.leftAdjointUniq
+
+-- Porting note (#10618): removed simp as simp can prove this
+theorem homEquiv_leftAdjointUniq_hom_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
+    (x : C) : adj1.homEquiv _ _ ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x := by
+  simp [leftAdjointUniq]
+#align category_theory.adjunction.hom_equiv_left_adjoint_uniq_hom_app CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app
+
+@[reassoc (attr := simp)]
+theorem unit_leftAdjointUniq_hom {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
+    adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G = adj2.unit := by
+  ext x
+  rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]
+  simp [← G.map_comp]
+#align category_theory.adjunction.unit_left_adjoint_uniq_hom CategoryTheory.Adjunction.unit_leftAdjointUniq_hom
+
+@[reassoc (attr := simp)]
+theorem unit_leftAdjointUniq_hom_app {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 :=
+  by rw [← unit_leftAdjointUniq_hom adj1 adj2]; rfl
+#align category_theory.adjunction.unit_left_adjoint_uniq_hom_app CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app
+
+@[reassoc (attr := simp)]
+theorem leftAdjointUniq_hom_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
+    whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit := by
+  ext x
+  simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom, natIsoEquiv_apply_inv,
+    Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app, natTransEquiv_apply_app, whiskerLeft_id',
+    Category.comp_id, Category.assoc]
+  rw [← adj1.counit_naturality, ← Category.assoc, ← F.map_comp]
+  simp
+#align category_theory.adjunction.left_adjoint_uniq_hom_counit CategoryTheory.Adjunction.leftAdjointUniq_hom_counit
+
+@[reassoc (attr := simp)]
+theorem leftAdjointUniq_hom_app_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
+    (x : D) :
+    (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x := by
+  rw [← leftAdjointUniq_hom_counit adj1 adj2]
+  rfl
+#align category_theory.adjunction.left_adjoint_uniq_hom_app_counit CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit
+
+theorem leftAdjointUniq_inv_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
+    (leftAdjointUniq adj1 adj2).inv.app x = (leftAdjointUniq adj2 adj1).hom.app x :=
+  rfl
+#align category_theory.adjunction.left_adjoint_uniq_inv_app CategoryTheory.Adjunction.leftAdjointUniq_inv_app
+
+@[reassoc (attr := simp)]
+theorem leftAdjointUniq_trans {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
+    (adj3 : F'' ⊣ G) :
+    (leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom =
+      (leftAdjointUniq adj1 adj3).hom := by
+  simp [leftAdjointUniq]
+#align category_theory.adjunction.left_adjoint_uniq_trans CategoryTheory.Adjunction.leftAdjointUniq_trans
+
+@[reassoc (attr := simp)]
+theorem leftAdjointUniq_trans_app {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
+    (adj3 : F'' ⊣ G) (x : C) :
+    (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x =
+      (leftAdjointUniq adj1 adj3).hom.app x := by
+  rw [← leftAdjointUniq_trans adj1 adj2 adj3]
+  rfl
+#align category_theory.adjunction.left_adjoint_uniq_trans_app CategoryTheory.Adjunction.leftAdjointUniq_trans_app
+
+@[simp]
+theorem leftAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
+    (leftAdjointUniq adj1 adj1).hom = 𝟙 _ := by
+  simp [leftAdjointUniq]
+#align category_theory.adjunction.left_adjoint_uniq_refl CategoryTheory.Adjunction.leftAdjointUniq_refl
+
+/-- If `G` and `G'` are both right adjoint to `F`, then they are naturally isomorphic. -/
+def rightAdjointUniq {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') : G ≅ G' :=
+  (natIsoEquiv adj1 adj2).symm (Iso.refl _)
+#align category_theory.adjunction.right_adjoint_uniq CategoryTheory.Adjunction.rightAdjointUniq
+
+-- Porting note (#10618): simp can prove this
+theorem homEquiv_symm_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G)
+    (adj2 : F ⊣ G') (x : D) :
+    (adj2.homEquiv _ _).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x := by
+  simp [rightAdjointUniq]
+#align category_theory.adjunction.hom_equiv_symm_right_adjoint_uniq_hom_app CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app
+
+@[reassoc (attr := simp)]
+theorem unit_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
+    (x : C) : adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x) =
+      adj2.unit.app x := by
+  simp only [Functor.id_obj, Functor.comp_obj, rightAdjointUniq, natIsoEquiv_symm_apply_hom,
+    Iso.refl_hom, natTransEquiv_symm_apply_app, NatTrans.id_app, Category.id_comp]
+  rw [← adj2.unit_naturality_assoc, ← G'.map_comp]
+  simp
+#align category_theory.adjunction.unit_right_adjoint_uniq_hom_app CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app
+
+@[reassoc (attr := simp)]
+theorem unit_rightAdjointUniq_hom {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
+    adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom = adj2.unit := by
+  ext x
+  simp
+#align category_theory.adjunction.unit_right_adjoint_uniq_hom CategoryTheory.Adjunction.unit_rightAdjointUniq_hom
+
+@[reassoc (attr := simp)]
+theorem rightAdjointUniq_hom_app_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
+    (x : D) :
+    F.map ((rightAdjointUniq adj1 adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x := by
+  simp [rightAdjointUniq]
+#align category_theory.adjunction.right_adjoint_uniq_hom_app_counit CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit
+
+@[reassoc (attr := simp)]
+theorem rightAdjointUniq_hom_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
+    whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit := by
+  ext
+  simp
+#align category_theory.adjunction.right_adjoint_uniq_hom_counit CategoryTheory.Adjunction.rightAdjointUniq_hom_counit
+
+theorem rightAdjointUniq_inv_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
+    (x : D) : (rightAdjointUniq adj1 adj2).inv.app x = (rightAdjointUniq adj2 adj1).hom.app x :=
+  rfl
+#align category_theory.adjunction.right_adjoint_uniq_inv_app CategoryTheory.Adjunction.rightAdjointUniq_inv_app
+
+@[reassoc (attr := simp)]
+theorem rightAdjointUniq_trans {F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
+    (adj3 : F ⊣ G'') :
+    (rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom =
+      (rightAdjointUniq adj1 adj3).hom := by
+  simp [rightAdjointUniq]
+#align category_theory.adjunction.right_adjoint_uniq_trans CategoryTheory.Adjunction.rightAdjointUniq_trans
+
+@[reassoc (attr := simp)]
+theorem rightAdjointUniq_trans_app {F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
+    (adj3 : F ⊣ G'') (x : D) :
+    (rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x =
+      (rightAdjointUniq adj1 adj3).hom.app x := by
+  rw [← rightAdjointUniq_trans adj1 adj2 adj3]
+  rfl
+#align category_theory.adjunction.right_adjoint_uniq_trans_app CategoryTheory.Adjunction.rightAdjointUniq_trans_app
+
+
+@[simp]
+theorem rightAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
+    (rightAdjointUniq adj1 adj1).hom = 𝟙 _ := by
+  delta rightAdjointUniq
+  simp
+#align category_theory.adjunction.right_adjoint_uniq_refl CategoryTheory.Adjunction.rightAdjointUniq_refl
diff --git a/Mathlib/CategoryTheory/Limits/Over.lean b/Mathlib/CategoryTheory/Limits/Over.lean
index 4d8af86f7b3e6..687d4db9c80c3 100644
--- a/Mathlib/CategoryTheory/Limits/Over.lean
+++ b/Mathlib/CategoryTheory/Limits/Over.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Reid Barton, Bhavik Mehta
 -/
-import Mathlib.CategoryTheory.Adjunction.Opposites
+import Mathlib.CategoryTheory.Adjunction.Unique
 import Mathlib.CategoryTheory.Comma.Over
 import Mathlib.CategoryTheory.Limits.Comma
 import Mathlib.CategoryTheory.Limits.ConeCategory
diff --git a/Mathlib/CategoryTheory/Limits/Presheaf.lean b/Mathlib/CategoryTheory/Limits/Presheaf.lean
index e058a3caa2e58..ace1c468f7b61 100644
--- a/Mathlib/CategoryTheory/Limits/Presheaf.lean
+++ b/Mathlib/CategoryTheory/Limits/Presheaf.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
+import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Comma.Presheaf
 import Mathlib.CategoryTheory.Elements
 import Mathlib.CategoryTheory.Limits.ConeCategory
diff --git a/Mathlib/CategoryTheory/Sites/CoverLifting.lean b/Mathlib/CategoryTheory/Sites/CoverLifting.lean
index 2b66ec443ed43..73ffa87122ebd 100644
--- a/Mathlib/CategoryTheory/Sites/CoverLifting.lean
+++ b/Mathlib/CategoryTheory/Sites/CoverLifting.lean
@@ -377,13 +377,15 @@ lemma Functor.toSheafify_pullbackSheafificationCompatibility (F : Dᵒᵖ ⥤ A)
     toSheafify J (G.op ⋙ F) ≫
     ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
     whiskerLeft _ (toSheafify K _) := by
-  dsimp [pushforwardContinuousSheafificationCompatibility, Adjunction.leftAdjointUniq]
+  dsimp [pushforwardContinuousSheafificationCompatibility]
+  simp only [Adjunction.leftAdjointUniq, Iso.symm_hom, Adjunction.natIsoEquiv_apply_inv,
+    Iso.refl_inv, Adjunction.natTransEquiv_apply_app, comp_obj, whiskeringLeft_obj_obj,
+    sheafToPresheaf_obj, whiskerLeft_id', Category.comp_id, comp_map, whiskeringLeft_obj_map,
+    Sheaf.instCategorySheaf_comp_val]
   apply Quiver.Hom.op_inj
   apply coyoneda.map_injective
   ext E : 2
-  dsimp [Functor.preimage, Coyoneda.preimage, coyoneda, Adjunction.leftAdjointsCoyonedaEquiv]
-  erw [Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]
-  dsimp [Adjunction.comp]
+  dsimp [Functor.preimage, Coyoneda.preimage, coyoneda, Adjunction.comp]
   simp only [Category.comp_id, map_id, whiskerLeft_id', map_comp, Sheaf.instCategorySheaf_comp_val,
     sheafificationAdjunction_counit_app_val, sheafifyMap_sheafifyLift,
     Category.id_comp, Category.assoc, toSheafify_sheafifyLift]
diff --git a/Mathlib/CategoryTheory/Sites/Sheafification.lean b/Mathlib/CategoryTheory/Sites/Sheafification.lean
index 2547e2053b259..a4b8787bcd034 100644
--- a/Mathlib/CategoryTheory/Sites/Sheafification.lean
+++ b/Mathlib/CategoryTheory/Sites/Sheafification.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
-import Mathlib.CategoryTheory.Adjunction.Opposites
+import Mathlib.CategoryTheory.Adjunction.Unique
 import Mathlib.CategoryTheory.Adjunction.FullyFaithful
 import Mathlib.CategoryTheory.Sites.Sheaf
 import Mathlib.CategoryTheory.Limits.Preserves.Finite
diff --git a/Mathlib/Order/Category/BddLat.lean b/Mathlib/Order/Category/BddLat.lean
index 77a570f86a34e..915ab9ddca3a0 100644
--- a/Mathlib/Order/Category/BddLat.lean
+++ b/Mathlib/Order/Category/BddLat.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.CategoryTheory.Adjunction.Opposites
+import Mathlib.CategoryTheory.Adjunction.Unique
 import Mathlib.Order.Category.BddOrd
 import Mathlib.Order.Category.Lat
 import Mathlib.Order.Category.Semilat
diff --git a/Mathlib/Topology/Sheaves/Presheaf.lean b/Mathlib/Topology/Sheaves/Presheaf.lean
index 0f62f78e0bcf4..9c9294373cf96 100644
--- a/Mathlib/Topology/Sheaves/Presheaf.lean
+++ b/Mathlib/Topology/Sheaves/Presheaf.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison, Mario Carneiro, Reid Barton, Andrew Yang
 -/
 import Mathlib.CategoryTheory.Limits.KanExtension
 import Mathlib.Topology.Category.TopCat.Opens
-import Mathlib.CategoryTheory.Adjunction.Opposites
+import Mathlib.CategoryTheory.Adjunction.Unique
 import Mathlib.Topology.Sheaves.Init
 import Mathlib.Data.Set.Subsingleton