chore: Homogenise instances for MulOpposite/AddOpposite (#11485)

by declaring them all in `where` style with implicit type assumptions and `inst` prefix

Here to reduce the diff from #11203

Mathlib/Algebra/Field/Opposite.lean

@@ -13,16 +13,14 @@ import Mathlib.Data.Int.Cast.Lemmas
 # Field structure on the multiplicative/additive opposite
 -/
 
-namespace MulOpposite
+variable {α : Type*}
 
-variable (α : Type*)
+namespace MulOpposite
 
 @[to_additive]
 instance ratCast [RatCast α] : RatCast αᵐᵒᵖ :=
   ⟨fun n => op n⟩
 
-variable {α}
-
 @[to_additive (attr := simp, norm_cast)]
 theorem op_ratCast [RatCast α] (q : ℚ) : op (q : α) = q :=
   rfl
@@ -35,44 +33,46 @@ theorem unop_ratCast [RatCast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q :=
 #align mul_opposite.unop_rat_cast MulOpposite.unop_ratCast
 #align add_opposite.unop_rat_cast AddOpposite.unop_ratCast
 
-variable (α)
+instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ where
+  __ := instSemiring
+  __ := instGroupWithZero
 
-instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ :=
-  { MulOpposite.instGroupWithZero α, MulOpposite.instSemiring α with }
+instance instDivisionRing [DivisionRing α] : DivisionRing αᵐᵒᵖ where
+  __ := instRing
+  __ := instDivisionSemiring
+  ratCast_mk a b hb h := unop_injective <| by rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv,
+    unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
+  qsmul := qsmulRec _
 
-instance instDivisionRing [DivisionRing α] : DivisionRing αᵐᵒᵖ :=
-  { MulOpposite.instDivisionSemiring α, MulOpposite.instRing α, MulOpposite.ratCast α with
-    ratCast_mk := fun a b hb h => unop_injective <| by
-      rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast,
-        Int.commute_cast, div_eq_mul_inv]
-    qsmul := qsmulRec _ }
+instance instSemifield [Semifield α] : Semifield αᵐᵒᵖ where
+  __ := instCommSemiring
+  __ := instDivisionSemiring
 
-instance instSemifield [Semifield α] : Semifield αᵐᵒᵖ :=
-  { MulOpposite.instDivisionSemiring α, MulOpposite.instCommSemiring α with }
-
-instance instField [Field α] : Field αᵐᵒᵖ :=
-  { MulOpposite.instDivisionRing α, MulOpposite.instCommRing α with }
+instance instField [Field α] : Field αᵐᵒᵖ where
+  __ := instCommRing
+  __ := instDivisionRing
 
 end MulOpposite
 
 namespace AddOpposite
 
-variable {α : Type*}
-
-instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ :=
-  { AddOpposite.instGroupWithZero α, AddOpposite.instSemiring α with }
+instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ where
+  __ := instSemiring
+  __ := instGroupWithZero
 
-instance instDivisionRing [DivisionRing α] : DivisionRing αᵃᵒᵖ :=
-  { AddOpposite.instRing α, AddOpposite.instGroupWithZero α, AddOpposite.ratCast α with
-    ratCast_mk := fun a b hb h => unop_injective <| by
-      rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast,
-        div_eq_mul_inv]
-    qsmul := qsmulRec _ }
+instance instDivisionRing [DivisionRing α] : DivisionRing αᵃᵒᵖ where
+  __ := instRing
+  __ := instDivisionSemiring
+  ratCast_mk a b hb h := unop_injective <| by rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv,
+    unop_natCast, unop_intCast, div_eq_mul_inv]
+  qsmul := _
 
-instance instSemifield [Semifield α] : Semifield αᵃᵒᵖ :=
-  { AddOpposite.instDivisionSemiring, AddOpposite.instCommSemiring α with }
+instance instSemifield [Semifield α] : Semifield αᵃᵒᵖ where
+  __ := instCommSemiring
+  __ := instDivisionSemiring
 
-instance instField [Field α] : Field αᵃᵒᵖ :=
-  { AddOpposite.instDivisionRing, AddOpposite.instCommRing α with }
+instance instField [Field α] : Field αᵃᵒᵖ where
+  __ := instCommRing
+  __ := instDivisionRing
 
 end AddOpposite