From c1b8a013aca976156a1317bff6fa8554a7e0092a Mon Sep 17 00:00:00 2001
From: morel <smorel@math.princeton.edu>
Date: Wed, 1 Jan 2025 12:35:54 +0100
Subject: [PATCH] make arguments implicit

---
 .../CategoryTheory/Adjunction/Opposites.lean  | 38 ++++---------------
 1 file changed, 7 insertions(+), 31 deletions(-)

diff --git a/Mathlib/CategoryTheory/Adjunction/Opposites.lean b/Mathlib/CategoryTheory/Adjunction/Opposites.lean
index bfb7166816fb0..9927857034e4b 100644
--- a/Mathlib/CategoryTheory/Adjunction/Opposites.lean
+++ b/Mathlib/CategoryTheory/Adjunction/Opposites.lean
@@ -38,46 +38,22 @@ def unop {F : Cᵒᵖ ⥤ Dᵒᵖ} {G : Dᵒᵖ ⥤ Cᵒᵖ} (h : G ⊣ F) : F.u
   right_triangle_components _ := Quiver.Hom.op_inj (h.left_triangle_components _)
 
 @[deprecated (since := "2025-01-01")] alias adjointOfOpAdjointOp := unop
-
-/-- If `G` is adjoint to `F.op` then `F` is adjoint to `G.unop`. -/
-@[deprecated "Use Adjunction.unop instead." (since := "2025-01-01")]
-def adjointUnopOfAdjointOp (F : C ⥤ D) (G : Dᵒᵖ ⥤ Cᵒᵖ) (h : G ⊣ F.op) : F ⊣ G.unop :=
-  unop F G.unop (h.ofNatIsoLeft G.opUnopIso.symm)
-
-/-- If `G.op` is adjoint to `F` then `F.unop` is adjoint to `G`. -/
-@[deprecated "Use Adjunction.unop instead." (since := "2025-01-01")]
-def unopAdjointOfOpAdjoint (F : Cᵒᵖ ⥤ Dᵒᵖ) (G : D ⥤ C) (h : G.op ⊣ F) : F.unop ⊣ G :=
-  unop _ _ (h.ofNatIsoRight F.opUnopIso.symm)
-
-/-- If `G` is adjoint to `F` then `F.unop` is adjoint to `G.unop`. -/
-@[deprecated "Use Adjunction.unop instead." (since := "2025-01-01")]
-def unopAdjointUnopOfAdjoint (F : Cᵒᵖ ⥤ Dᵒᵖ) (G : Dᵒᵖ ⥤ Cᵒᵖ) (h : G ⊣ F) : F.unop ⊣ G.unop :=
-  unop F.unop G.unop (h.ofNatIsoRight F.opUnopIso.symm)
+@[deprecated (since := "2025-01-01")] alias adjointUnopOfAdjointOp := unop
+@[deprecated (since := "2025-01-01")] alias unopAdjointOfOpAdjoint := unop
+@[deprecated (since := "2025-01-01")] alias unopAdjointUnopOfAdjoint := unop
 
 /-- If `G` is adjoint to `F` then `F.op` is adjoint to `G.op`. -/
 @[simps]
-def op (F : C ⥤ D) (G : D ⥤ C) (h : G ⊣ F) : F.op ⊣ G.op where
+def op {F : C ⥤ D} {G : D ⥤ C} (h : G ⊣ F) : F.op ⊣ G.op where
   unit := NatTrans.op h.counit
   counit := NatTrans.op h.unit
   left_triangle_components _ := Quiver.Hom.unop_inj (by simp)
   right_triangle_components _ := Quiver.Hom.unop_inj (by simp)
 
 @[deprecated (since := "2025-01-01")] alias opAdjointOpOfAdjoint := op
-
-/-- If `G` is adjoint to `F.unop` then `F` is adjoint to `G.op`. -/
-@[deprecated "Use Adjunction.op instead." (since := "2025-01-01")]
-def adjointOpOfAdjointUnop (F : Cᵒᵖ ⥤ Dᵒᵖ) (G : D ⥤ C) (h : G ⊣ F.unop) : F ⊣ G.op :=
-  (op F.unop _ h).ofNatIsoLeft F.opUnopIso
-
-/-- If `G.unop` is adjoint to `F` then `F.op` is adjoint to `G`. -/
-@[deprecated "Use Adjunction.op instead." (since := "2025-01-01")]
-def opAdjointOfUnopAdjoint (F : C ⥤ D) (G : Dᵒᵖ ⥤ Cᵒᵖ) (h : G.unop ⊣ F) : F.op ⊣ G :=
-  (op _ G.unop h).ofNatIsoRight G.opUnopIso
-
-/-- If `G.unop` is adjoint to `F.unop` then `F` is adjoint to `G`. -/
-@[deprecated "Use Adjunction.op instead." (since := "2025-01-01")]
-def adjointOfUnopAdjointUnop (F : Cᵒᵖ ⥤ Dᵒᵖ) (G : Dᵒᵖ ⥤ Cᵒᵖ) (h : G.unop ⊣ F.unop) : F ⊣ G :=
-  (op _ _ h).ofNatIsoRight G.opUnopIso
+@[deprecated (since := "2025-01-01")] alias adjointOpOfAdjointUnop := op
+@[deprecated (since := "2025-01-01")] alias opAdjointOfUnopAdjoint := op
+@[deprecated (since := "2025-01-01")] alias adjointOfUnopAdjointUnop := op
 
 /-- If `F` and `F'` are both adjoint to `G`, there is a natural isomorphism
 `F.op ⋙ coyoneda ≅ F'.op ⋙ coyoneda`.