diff --git a/src/category_theory/adjunction/opposites.lean b/src/category_theory/adjunction/opposites.lean
index 45bd32f1334c1..99c9fc73f1426 100644
--- a/src/category_theory/adjunction/opposites.lean
+++ b/src/category_theory/adjunction/opposites.lean
@@ -1,7 +1,7 @@
 /-
 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
+Authors: Bhavik Mehta, Thomas Read, Andrew Yang
 -/
 
 import category_theory.adjunction.basic
@@ -29,7 +29,7 @@ variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D
 namespace adjunction
 
 /-- If `G.op` is adjoint to `F.op` then `F` is adjoint to `G`. -/
-def adjoint_of_op_adjoint_op (F : C ⥤ D) (G : D ⥤ C) (h : G.op ⊣ F.op) : F ⊣ G :=
+@[simps] def adjoint_of_op_adjoint_op (F : C ⥤ D) (G : D ⥤ C) (h : G.op ⊣ F.op) : F ⊣ G :=
 adjunction.mk_of_hom_equiv
 { hom_equiv := λ X Y,
   ((h.hom_equiv (opposite.op Y) (opposite.op X)).trans (op_equiv _ _)).symm.trans (op_equiv _ _) }
@@ -47,7 +47,7 @@ def unop_adjoint_unop_of_adjoint (F : Cᵒᵖ ⥤ Dᵒᵖ) (G : Dᵒᵖ ⥤ Cᵒ
 adjoint_unop_of_adjoint_op F.unop G (h.of_nat_iso_right F.op_unop_iso.symm)
 
 /-- If `G` is adjoint to `F` then `F.op` is adjoint to `G.op`. -/
-def op_adjoint_op_of_adjoint (F : C ⥤ D) (G : D ⥤ C) (h : G ⊣ F) : F.op ⊣ G.op :=
+@[simps] def op_adjoint_op_of_adjoint (F : C ⥤ D) (G : D ⥤ C) (h : G ⊣ F) : F.op ⊣ G.op :=
 adjunction.mk_of_hom_equiv
 { hom_equiv := λ X Y,
   (op_equiv _ Y).trans ((h.hom_equiv _ _).symm.trans (op_equiv X (opposite.op _)).symm) }
@@ -83,12 +83,170 @@ def left_adjoint_uniq {F F' : C ⥤ D} {G : D ⥤ C}
   (adj1 : F ⊣ G) (adj2 : F' ⊣ G) : F ≅ F' :=
 nat_iso.remove_op (fully_faithful_cancel_right _ (left_adjoints_coyoneda_equiv adj2 adj1))
 
+@[simp]
+lemma hom_equiv_left_adjoint_uniq_hom_app {F F' : C ⥤ D} {G : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
+  adj1.hom_equiv _ _ ((left_adjoint_uniq adj1 adj2).hom.app x) = adj2.unit.app x :=
+begin
+  apply (adj1.hom_equiv _ _).symm.injective,
+  apply quiver.hom.op_inj,
+  apply coyoneda.map_injective,
+  swap, apply_instance,
+  ext f y,
+  simpa [left_adjoint_uniq, left_adjoints_coyoneda_equiv]
+end
+
+@[simp, reassoc]
+lemma unit_left_adjoint_uniq_hom {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
+  adj1.unit ≫ whisker_right (left_adjoint_uniq adj1 adj2).hom G = adj2.unit :=
+begin
+  ext x,
+  rw [nat_trans.comp_app, ← hom_equiv_left_adjoint_uniq_hom_app adj1 adj2],
+  simp [-hom_equiv_left_adjoint_uniq_hom_app, ←G.map_comp]
+end
+
+@[simp, reassoc]
+lemma unit_left_adjoint_uniq_hom_app {F F' : C ⥤ D} {G : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
+  adj1.unit.app x ≫ G.map ((left_adjoint_uniq adj1 adj2).hom.app x) = adj2.unit.app x :=
+by { rw ← unit_left_adjoint_uniq_hom adj1 adj2, refl }
+
+@[simp, reassoc]
+lemma left_adjoint_uniq_hom_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
+  whisker_left G (left_adjoint_uniq adj1 adj2).hom ≫ adj2.counit = adj1.counit :=
+begin
+  ext x,
+  apply quiver.hom.op_inj,
+  apply coyoneda.map_injective,
+  swap, apply_instance,
+  ext y f,
+  have : F.map (adj2.unit.app (G.obj x)) ≫ adj1.counit.app (F'.obj (G.obj x)) ≫
+    adj2.counit.app x ≫ f = adj1.counit.app x ≫ f,
+  { erw [← adj1.counit.naturality, ← F.map_comp_assoc], simpa },
+  simpa [left_adjoint_uniq, left_adjoints_coyoneda_equiv] using this
+end
+
+@[simp, reassoc]
+lemma left_adjoint_uniq_hom_app_counit {F F' : C ⥤ D} {G : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : D) :
+  (left_adjoint_uniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x :=
+by { rw ← left_adjoint_uniq_hom_counit adj1 adj2, refl }
+
+@[simp]
+lemma left_adjoint_uniq_inv_app {F F' : C ⥤ D} {G : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
+  (left_adjoint_uniq adj1 adj2).inv.app x = (left_adjoint_uniq adj2 adj1).hom.app x := rfl
+
+@[simp, reassoc]
+lemma left_adjoint_uniq_trans {F F' F'' : C ⥤ D} {G : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) :
+  (left_adjoint_uniq adj1 adj2).hom ≫ (left_adjoint_uniq adj2 adj3).hom =
+    (left_adjoint_uniq adj1 adj3).hom :=
+begin
+  ext,
+  apply quiver.hom.op_inj,
+  apply coyoneda.map_injective,
+  swap, apply_instance,
+  ext,
+  simp [left_adjoints_coyoneda_equiv, left_adjoint_uniq]
+end
+
+@[simp, reassoc]
+lemma left_adjoint_uniq_trans_app {F F' F'' : C ⥤ D} {G : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) (x : C) :
+  (left_adjoint_uniq adj1 adj2).hom.app x ≫ (left_adjoint_uniq adj2 adj3).hom.app x =
+    (left_adjoint_uniq adj1 adj3).hom.app x :=
+by { rw ← left_adjoint_uniq_trans adj1 adj2 adj3, refl }
+
+@[simp]
+lemma left_adjoint_uniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
+  (left_adjoint_uniq adj1 adj1).hom = 𝟙 _ :=
+begin
+  ext,
+  apply quiver.hom.op_inj,
+  apply coyoneda.map_injective,
+  swap, apply_instance,
+  ext,
+  simp [left_adjoints_coyoneda_equiv, left_adjoint_uniq]
+end
+
 /-- If `G` and `G'` are both right adjoint to `F`, then they are naturally isomorphic. -/
 def right_adjoint_uniq {F : C ⥤ D} {G G' : D ⥤ C}
   (adj1 : F ⊣ G) (adj2 : F ⊣ G') : G ≅ G' :=
 nat_iso.remove_op
   (left_adjoint_uniq (op_adjoint_op_of_adjoint _ F adj2) (op_adjoint_op_of_adjoint _ _ adj1))
 
+@[simp]
+lemma hom_equiv_symm_right_adjoint_uniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) :
+  (adj2.hom_equiv _ _).symm ((right_adjoint_uniq adj1 adj2).hom.app x) = adj1.counit.app x :=
+begin
+  apply quiver.hom.op_inj,
+  convert hom_equiv_left_adjoint_uniq_hom_app
+    (op_adjoint_op_of_adjoint _ F adj2) (op_adjoint_op_of_adjoint _ _ adj1) (opposite.op x),
+  simpa
+end
+
+@[simp, reassoc]
+lemma unit_right_adjoint_uniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : C) :
+  adj1.unit.app x ≫ (right_adjoint_uniq adj1 adj2).hom.app (F.obj x) = adj2.unit.app x :=
+begin
+  apply quiver.hom.op_inj,
+  convert left_adjoint_uniq_hom_app_counit
+    (op_adjoint_op_of_adjoint _ _ adj2) (op_adjoint_op_of_adjoint _ _ adj1) (opposite.op x),
+  all_goals { simpa }
+end
+
+@[simp, reassoc]
+lemma unit_right_adjoint_uniq_hom {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
+  adj1.unit ≫ whisker_left F (right_adjoint_uniq adj1 adj2).hom = adj2.unit :=
+by { ext x, simp }
+
+@[simp, reassoc]
+lemma right_adjoint_uniq_hom_app_counit {F : C ⥤ D} {G G' : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) :
+  F.map ((right_adjoint_uniq adj1 adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x :=
+begin
+  apply quiver.hom.op_inj,
+  convert unit_left_adjoint_uniq_hom_app
+    (op_adjoint_op_of_adjoint _ _ adj2) (op_adjoint_op_of_adjoint _ _ adj1) (opposite.op x),
+  all_goals { simpa }
+end
+
+@[simp, reassoc]
+lemma right_adjoint_uniq_hom_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
+  whisker_right (right_adjoint_uniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit :=
+by { ext, simp }
+
+@[simp]
+lemma right_adjoint_uniq_inv_app {F : C ⥤ D} {G G' : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) :
+  (right_adjoint_uniq adj1 adj2).inv.app x = (right_adjoint_uniq adj2 adj1).hom.app x := rfl
+
+@[simp, reassoc]
+lemma right_adjoint_uniq_trans_app {F : C ⥤ D} {G G' G'' : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') (x : D) :
+  (right_adjoint_uniq adj1 adj2).hom.app x ≫ (right_adjoint_uniq adj2 adj3).hom.app x =
+    (right_adjoint_uniq adj1 adj3).hom.app x :=
+begin
+  apply quiver.hom.op_inj,
+  exact left_adjoint_uniq_trans_app (op_adjoint_op_of_adjoint _ _ adj3)
+    (op_adjoint_op_of_adjoint _ _ adj2) (op_adjoint_op_of_adjoint _ _ adj1) (opposite.op x)
+end
+
+@[simp, reassoc]
+lemma right_adjoint_uniq_trans {F : C ⥤ D} {G G' G'' : D ⥤ C}
+  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') :
+  (right_adjoint_uniq adj1 adj2).hom ≫ (right_adjoint_uniq adj2 adj3).hom =
+    (right_adjoint_uniq adj1 adj3).hom :=
+by { ext, simp }
+
+@[simp]
+lemma right_adjoint_uniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
+  (right_adjoint_uniq adj1 adj1).hom = 𝟙 _ :=
+by { delta right_adjoint_uniq, simp }
+
 /--
 Given two adjunctions, if the left adjoints are naturally isomorphic, then so are the right
 adjoints.