chore: Final cleanup before NNRat.cast

YaelDillies · YaelDillies · commit 194033db8230 · 2024-04-23T07:45:16.000Z
This is the parts of the diff of #11203 which don't mention `NNRat.cast`. * Use more `where` notation. * Write `qsmul := _` instead of `qsmul := qsmulRec _`. * Move `qsmul` before `ratCast_def` in instance declarations. * Name more instances. * Rename `rat_smul` to `qsmul`. *
diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean
@@ -1005,13 +1005,13 @@ protected theorem inv_mul_cancel {p : Ring.DirectLimit G f} (hp : p ≠ 0) : inv
 See note [reducible non-instances]. -/
 @[reducible]
 protected noncomputable def field [DirectedSystem G fun i j h => f' i j h] :
-    Field (Ring.DirectLimit G fun i j h => f' i j h) :=
+    Field (Ring.DirectLimit G fun i j h => f' i j h) where
   -- This used to include the parent CommRing and Nontrivial instances,
   -- but leaving them implicit avoids a very expensive (2-3 minutes!) eta expansion.
-  { inv := inv G fun i j h => f' i j h
-    mul_inv_cancel := fun p => DirectLimit.mul_inv_cancel G fun i j h => f' i j h
-    inv_zero := dif_pos rfl
-    qsmul := qsmulRec _ }
+  inv := inv G fun i j h => f' i j h
+  mul_inv_cancel := fun p => DirectLimit.mul_inv_cancel G fun i j h => f' i j h
+  inv_zero := dif_pos rfl
+  qsmul := _
 #align field.direct_limit.field Field.DirectLimit.field
 
 end
diff --git a/Mathlib/Algebra/Field/IsField.lean b/Mathlib/Algebra/Field/IsField.lean
@@ -63,13 +63,12 @@ theorem not_isField_of_subsingleton (R : Type u) [Semiring R] [Subsingleton R] :
 open scoped Classical
 
 /-- Transferring from `IsField` to `Semifield`. -/
-noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R) : Semifield R :=
-  { ‹Semiring R›, h with
-    inv := fun a => if ha : a = 0 then 0 else Classical.choose (IsField.mul_inv_cancel h ha),
-    inv_zero := dif_pos rfl,
-    mul_inv_cancel := fun a ha => by
-      convert Classical.choose_spec (IsField.mul_inv_cancel h ha)
-      exact dif_neg ha }
+noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R) : Semifield R where
+  __ := ‹Semiring R›
+  __ := h
+  inv a := if ha : a = 0 then 0 else Classical.choose (h.mul_inv_cancel ha)
+  inv_zero := dif_pos rfl
+  mul_inv_cancel a ha := by convert Classical.choose_spec (h.mul_inv_cancel ha); exact dif_neg ha
 #align is_field.to_semifield IsField.toSemifield
 
 /-- Transferring from `IsField` to `Field`. -/
diff --git a/Mathlib/Algebra/Field/ULift.lean b/Mathlib/Algebra/Field/ULift.lean
@@ -21,16 +21,11 @@ variable {α : Type u} {x y : ULift.{v} α}
 
 namespace ULift
 
-instance [RatCast α] : RatCast (ULift α) := ⟨(up ·)⟩
+instance instRatCast [RatCast α] : RatCast (ULift α) := ⟨fun a ↦ up a⟩
 
-@[simp, norm_cast]
-theorem up_ratCast [RatCast α] (q : ℚ) : up (q : α) = q :=
-  rfl
+@[simp, norm_cast] lemma up_ratCast [RatCast α] (q : ℚ) : up (q : α) = q := rfl
+@[simp, norm_cast] lemma down_ratCast [RatCast α] (q : ℚ) : down (q : ULift α) = q := rfl
 #align ulift.up_rat_cast ULift.up_ratCast
-
-@[simp, norm_cast]
-theorem down_ratCast [RatCast α] (q : ℚ) : down (q : ULift α) = q :=
-  rfl
 #align ulift.down_rat_cast ULift.down_ratCast
 
 instance divisionSemiring [DivisionSemiring α] : DivisionSemiring (ULift α) := by
diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean
@@ -203,12 +203,9 @@ section
 variable {α : Type*} [LinearOrderedField α]
 variable {β : Type*} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv]
 
-instance : RatCast (Cauchy abv) :=
-  ⟨fun q => ofRat q⟩
+instance instRatCast : RatCast (Cauchy abv) where ratCast q := ofRat q
 
-@[simp, coe]
-theorem ofRat_ratCast (q : ℚ) : ofRat (↑q : β) = (q : (Cauchy abv)) :=
-  rfl
+@[simp, norm_cast] lemma ofRat_ratCast (q : ℚ) : ofRat (q : β) = (q : Cauchy abv) := rfl
 #align cau_seq.completion.of_rat_rat_cast CauSeq.Completion.ofRat_ratCast
 
 noncomputable instance : Inv (Cauchy abv) :=
@@ -275,8 +272,8 @@ noncomputable instance Cauchy.divisionRing : DivisionRing (Cauchy abv) where
   exists_pair_ne := ⟨0, 1, zero_ne_one⟩
   inv_zero := inv_zero
   mul_inv_cancel x := CauSeq.Completion.mul_inv_cancel
-  ratCast_def q := by rw [← ofRat_ratCast, Rat.cast_def, ofRat_div, ofRat_natCast, ofRat_intCast]
   qsmul := (· • ·)
+  ratCast_def q := by rw [← ofRat_ratCast, Rat.cast_def, ofRat_div, ofRat_natCast, ofRat_intCast]
   qsmul_def q x := Quotient.inductionOn x fun f ↦ congr_arg mk <| ext fun i ↦ Rat.smul_def _ _
 
 /-- Show the first 10 items of a representative of this equivalence class of cauchy sequences.
diff --git a/Mathlib/Algebra/Polynomial/Basic.lean b/Mathlib/Algebra/Polynomial/Basic.lean
@@ -1263,9 +1263,9 @@ section DivisionRing
 
 variable [DivisionRing R]
 
-theorem rat_smul_eq_C_mul (a : ℚ) (f : R[X]) : a • f = Polynomial.C (a : R) * f := by
+theorem qsmul_eq_C_mul (a : ℚ) (f : R[X]) : a • f = Polynomial.C (a : R) * f := by
   rw [← Rat.smul_one_eq_coe, ← Polynomial.smul_C, C_1, smul_one_mul]
-#align polynomial.rat_smul_eq_C_mul Polynomial.rat_smul_eq_C_mul
+#align polynomial.rat_smul_eq_C_mul Polynomial.qsmul_eq_C_mul
 
 end DivisionRing
 
diff --git a/Mathlib/CategoryTheory/Preadditive/Schur.lean b/Mathlib/CategoryTheory/Preadditive/Schur.lean
@@ -58,25 +58,19 @@ theorem isIso_iff_nonzero [HasKernels C] {X Y : C} [Simple X] [Simple Y] (f : X
    fun w => isIso_of_hom_simple w⟩
 #align category_theory.is_iso_iff_nonzero CategoryTheory.isIso_iff_nonzero
 
+open scoped Classical in
 /-- In any preadditive category with kernels,
-the endomorphisms of a simple object form a division ring.
--/
-noncomputable instance [HasKernels C] {X : C} [Simple X] : DivisionRing (End X) := by
-  classical exact
-    { (inferInstance : Ring (End X)) with
-      inv := fun f =>
-        if h : f = 0 then 0
-        else
-          haveI := isIso_of_hom_simple h
-          inv f
-      exists_pair_ne := ⟨𝟙 X, 0, id_nonzero _⟩
-      inv_zero := dif_pos rfl
-      mul_inv_cancel := fun f h => by
-        dsimp
-        rw [dif_neg h]
-        haveI := isIso_of_hom_simple h
-        exact IsIso.inv_hom_id f
-      qsmul := qsmulRec _ }
+the endomorphisms of a simple object form a division ring. -/
+noncomputable instance [HasKernels C] {X : C} [Simple X] : DivisionRing (End X) where
+  inv f := if h : f = 0 then 0 else haveI := isIso_of_hom_simple h; inv f
+  exists_pair_ne := ⟨𝟙 X, 0, id_nonzero _⟩
+  inv_zero := dif_pos rfl
+  mul_inv_cancel f hf := by
+    dsimp
+    rw [dif_neg hf]
+    haveI := isIso_of_hom_simple hf
+    exact IsIso.inv_hom_id f
+  qsmul := _
 
 open FiniteDimensional
 
diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean
@@ -818,8 +818,8 @@ lemma div_im (z w : ℂ) : (z / w).im = z.im * w.re / normSq w - z.re * w.im / n
 noncomputable instance instField : Field ℂ where
   mul_inv_cancel := @Complex.mul_inv_cancel
   inv_zero := Complex.inv_zero
-  ratCast_def q := by ext <;> simp [Rat.cast_def, div_re, div_im, mul_div_mul_comm]
   qsmul := (· • ·)
+  ratCast_def q := by ext <;> simp [Rat.cast_def, div_re, div_im, mul_div_mul_comm]
   qsmul_def n z := ext_iff.2 <| by simp [Rat.smul_def, smul_re, smul_im]
 #align complex.field Complex.instField
 
diff --git a/Mathlib/Data/Rat/Field.lean b/Mathlib/Data/Rat/Field.lean
@@ -38,8 +38,8 @@ namespace Rat
 instance instField : Field ℚ where
   __ := commRing
   __ := commGroupWithZero
-  ratCast_def q := (num_div_den _).symm
   qsmul := _
+  ratCast_def q := (num_div_den _).symm
 
 -- Extra instances to short-circuit type class resolution
 instance instDivisionRing : DivisionRing ℚ := by infer_instance
diff --git a/Mathlib/Data/Real/Basic.lean b/Mathlib/Data/Real/Basic.lean
@@ -573,9 +573,9 @@ noncomputable instance instLinearOrderedField : LinearOrderedField ℝ where
       Ne, ofCauchy.injEq] at *
     exact CauSeq.Completion.inv_mul_cancel h
   inv_zero := by simp [← ofCauchy_zero, ← ofCauchy_inv]
+  qsmul := _
   ratCast_def q := by
     rw [← ofCauchy_ratCast, Rat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_intCast]
-  qsmul := _
 
 -- Extra instances to short-circuit type class resolution
 noncomputable instance : LinearOrderedAddCommGroup ℝ := by infer_instance
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
@@ -1245,12 +1245,10 @@ private theorem mul_inv_cancel_aux (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1 :
   rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
 
 /-- Field structure on `ZMod p` if `p` is prime. -/
-instance : Field (ZMod p) :=
-  { inferInstanceAs (CommRing (ZMod p)), inferInstanceAs (Inv (ZMod p)),
-    ZMod.nontrivial p with
-    mul_inv_cancel := mul_inv_cancel_aux p
-    inv_zero := inv_zero p
-    qsmul := qsmulRec _ }
+instance : Field (ZMod p) where
+  mul_inv_cancel := mul_inv_cancel_aux p
+  inv_zero := inv_zero p
+  qsmul := _
 
 /-- `ZMod p` is an integral domain when `p` is prime. -/
 instance (p : ℕ) [hp : Fact p.Prime] : IsDomain (ZMod p) := by
diff --git a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
@@ -434,9 +434,9 @@ instance instField : Field (AlgebraicClosure k) where
   __ := instCommRing _
   __ := instGroupWithZero _
   ratCast q := algebraMap k _ q
+  qsmul := (· • ·)
   ratCast_def q := by
     change algebraMap k _ _ = _; rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
-  qsmul := (· • ·)
   qsmul_def q x := Quotient.inductionOn x fun p ↦ congr_arg Quotient.mk'' $ by
     ext; simp [MvPolynomial.algebraMap_eq, Rat.smul_def]
 
diff --git a/Mathlib/FieldTheory/PerfectClosure.lean b/Mathlib/FieldTheory/PerfectClosure.lean
@@ -498,20 +498,16 @@ theorem mk_inv (x : ℕ × K) : (mk K p x)⁻¹ = mk K p (x.1, x.2⁻¹) :=
   rfl
 
 -- Porting note: added to avoid "unknown free variable" error
-instance instDivisionRing : DivisionRing (PerfectClosure K p) :=
-  { (inferInstance : Inv (PerfectClosure K p)) with
-    exists_pair_ne := ⟨0, 1, fun H => zero_ne_one ((eq_iff _ _ _ _).1 H)⟩
-    mul_inv_cancel := fun e =>
-      induction_on e fun ⟨m, x⟩ H => by
-        -- Porting note: restructured
-        have := mt (eq_iff _ _ _ _).2 H
-        rw [mk_inv, mk_mul_mk]
-        refine (eq_iff K p _ _).2 ?_
-        simp only [iterate_map_one, iterate_map_zero,
-            iterate_zero_apply, ← iterate_map_mul] at this ⊢
-        rw [mul_inv_cancel this, iterate_map_one]
-    inv_zero := congr_arg (Quot.mk (R K p)) (by rw [inv_zero])
-    qsmul := qsmulRec _ }
+instance instDivisionRing : DivisionRing (PerfectClosure K p) where
+  exists_pair_ne := ⟨0, 1, fun H => zero_ne_one ((eq_iff _ _ _ _).1 H)⟩
+  mul_inv_cancel e := induction_on e fun ⟨m, x⟩ H => by
+    have := mt (eq_iff _ _ _ _).2 H
+    rw [mk_inv, mk_mul_mk]
+    refine (eq_iff K p _ _).2 ?_
+    simp only [iterate_map_one, iterate_map_zero, iterate_zero_apply, ← iterate_map_mul] at this ⊢
+    rw [mul_inv_cancel this, iterate_map_one]
+  inv_zero := congr_arg (Quot.mk (R K p)) (by rw [inv_zero])
+  qsmul := _
 
 instance instField : Field (PerfectClosure K p) :=
   { (inferInstance : DivisionRing (PerfectClosure K p)),
diff --git a/Mathlib/FieldTheory/RatFunc.lean b/Mathlib/FieldTheory/RatFunc.lean
@@ -780,16 +780,14 @@ end LiftHom
 
 variable (K)
 
-instance instField [IsDomain K] : Field (RatFunc K) :=
-  { RatFunc.instCommRing K, RatFunc.instNontrivial K with
-    inv := Inv.inv
-    -- Porting note: used to be `by frac_tac`
-    inv_zero := by rw [← ofFractionRing_zero, ← ofFractionRing_inv, inv_zero]
-    div := (· / ·)
-    div_eq_mul_inv := by frac_tac
-    mul_inv_cancel := fun _ => mul_inv_cancel
-    zpow := zpowRec
-    qsmul := qsmulRec _ }
+instance instField [IsDomain K] : Field (RatFunc K) where
+  -- Porting note: used to be `by frac_tac`
+  inv_zero := by rw [← ofFractionRing_zero, ← ofFractionRing_inv, inv_zero]
+  div := (· / ·)
+  div_eq_mul_inv := by frac_tac
+  mul_inv_cancel _ := mul_inv_cancel
+  zpow := zpowRec
+  qsmul := _
 
 section IsFractionRing
 
diff --git a/Mathlib/FieldTheory/SplittingField/Construction.lean b/Mathlib/FieldTheory/SplittingField/Construction.lean
@@ -278,9 +278,9 @@ instance instField : Field (SplittingField f) where
   __ := commRing _
   __ := instGroupWithZero _
   ratCast q := algebraMap K _ q
+  qsmul := (· • ·)
   ratCast_def q := by
     change algebraMap K _ _ = _; rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
-  qsmul := (· • ·)
   qsmul_def q x := Quotient.inductionOn x fun p ↦ congr_arg Quotient.mk'' $ by
     ext; simp [MvPolynomial.algebraMap_eq, Rat.smul_def]
 
diff --git a/Mathlib/FieldTheory/Subfield.lean b/Mathlib/FieldTheory/Subfield.lean
@@ -93,34 +93,30 @@ lemma ratCast_mem (s : S) (q : ℚ) : (q : K) ∈ s := by
   simpa only [Rat.cast_def] using div_mem (intCast_mem s q.num) (natCast_mem s q.den)
 #align subfield_class.coe_rat_mem SubfieldClass.ratCast_mem
 
-instance (s : S) : RatCast s :=
-  ⟨fun x => ⟨↑x, ratCast_mem s x⟩⟩
+instance instRatCast (s : S) : RatCast s where ratCast q := ⟨q, ratCast_mem s q⟩
 
 @[simp, norm_cast] lemma coe_ratCast (s : S) (x : ℚ) : ((x : s) : K) = x := rfl
 #align subfield_class.coe_rat_cast SubfieldClass.coe_ratCast
 
+@[aesop safe apply (rule_sets := [SetLike])]
+lemma qsmul_mem (s : S) (q : ℚ) (hx : x ∈ s) : q • x ∈ s := by
+  simpa only [Rat.smul_def] using mul_mem (ratCast_mem _ _) hx
+#align subfield_class.rat_smul_mem SubfieldClass.qsmul_mem
+
 -- 2024-04-05
 @[deprecated] alias coe_rat_cast := coe_ratCast
 @[deprecated] alias coe_rat_mem := ratCast_mem
-
--- Porting note: Mistranslated: used to be (a • x : K) ∈ s
-@[aesop safe apply (rule_sets := [SetLike])]
-theorem rat_smul_mem (s : S) (a : ℚ) (x : s) : a • (x : K) ∈ s := by
-  simpa only [Rat.smul_def] using mul_mem (ratCast_mem s a) x.prop
-#align subfield_class.rat_smul_mem SubfieldClass.rat_smul_mem
+@[deprecated] alias rat_smul_mem := qsmul_mem
 
 @[aesop safe apply (rule_sets := [SetLike])]
 lemma ofScientific_mem (s : S) {b : Bool} {n m : ℕ} :
     (OfScientific.ofScientific n b m : K) ∈ s :=
   SubfieldClass.ratCast_mem ..
 
-instance (s : S) : SMul ℚ s :=
-  ⟨fun a x => ⟨a • (x : K), rat_smul_mem s a x⟩⟩
+instance instSMulRat (s : S) : SMul ℚ s where smul q x := ⟨q • x, qsmul_mem s q x.2⟩
 
-@[simp]
-theorem coe_rat_smul (s : S) (a : ℚ) (x : s) : ↑(a • x) = a • (x : K) :=
-  rfl
-#align subfield_class.coe_rat_smul SubfieldClass.coe_rat_smul
+@[simp, norm_cast] lemma coe_qsmul (s : S) (q : ℚ) (x : s) : ↑(q • x) = q • (x : K) := rfl
+#align subfield_class.coe_rat_smul SubfieldClass.coe_qsmul
 
 variable (S)
 
@@ -342,6 +338,7 @@ instance : Inv s :=
 instance : Pow s ℤ :=
   ⟨fun x z => ⟨x ^ z, s.zpow_mem x.2 z⟩⟩
 
+-- TODO: Those are just special cases of `SubfieldClass.toDivisionRing`/`SubfieldClass.toField`
 instance toDivisionRing (s : Subfield K) : DivisionRing s :=
   Subtype.coe_injective.divisionRing ((↑) : s → K) rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
     (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean
@@ -859,19 +859,17 @@ lemma FiniteDimensional.exists_mul_eq_one (F : Type*) {K : Type*} [Field F] [Rin
   exact this 1
 
 /-- A domain that is module-finite as an algebra over a field is a division ring. -/
-noncomputable def divisionRingOfFiniteDimensional (F K : Type*) [Field F] [h : Ring K] [IsDomain K]
-    [Algebra F K] [FiniteDimensional F K] : DivisionRing K :=
-  { ‹IsDomain K› with
-    toRing := h
-    inv := fun x =>
-      letI := Classical.decEq K
-      if H : x = 0 then 0 else Classical.choose <| FiniteDimensional.exists_mul_eq_one F H
-    mul_inv_cancel := fun x hx =>
-      show x * dite _ (h := _) _ = _ by
-        rw [dif_neg hx]
-        exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)
-    inv_zero := dif_pos rfl
-    qsmul := qsmulRec _ }
+noncomputable def divisionRingOfFiniteDimensional (F K : Type*) [Field F] [Ring K] [IsDomain K]
+    [Algebra F K] [FiniteDimensional F K] : DivisionRing K where
+  __ := ‹IsDomain K›
+  inv x :=
+    letI := Classical.decEq K
+    if H : x = 0 then 0 else Classical.choose <| FiniteDimensional.exists_mul_eq_one F H
+  mul_inv_cancel x hx := show x * dite _ (h := _) _ = _ by
+    rw [dif_neg hx]
+    exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)
+  inv_zero := dif_pos rfl
+  qsmul := _
 #align division_ring_of_finite_dimensional divisionRingOfFiniteDimensional
 
 /-- An integral domain that is module-finite as an algebra over a field is a field. -/
diff --git a/Mathlib/Logic/Equiv/TransferInstance.lean b/Mathlib/Logic/Equiv/TransferInstance.lean
@@ -561,8 +561,7 @@ noncomputable instance [Small.{v} α] [Ring α] [IsDomain α] : IsDomain (Shrink
   Equiv.isDomain  (Shrink.ringEquiv α)
 
 /-- Transfer `RatCast` across an `Equiv` -/
-@[reducible]
-protected def ratCast [RatCast β] : RatCast α where ratCast n := e.symm n
+@[reducible] protected def ratCast [RatCast β] : RatCast α where ratCast n := e.symm n
 #align equiv.has_rat_cast Equiv.ratCast
 
 noncomputable instance _root_.Shrink.instRatCast [Small.{v} α] [RatCast α] :
diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean
@@ -396,13 +396,13 @@ noncomputable instance instGroupWithZero [Fact (Irreducible f)] : GroupWithZero
 noncomputable instance instField [Fact (Irreducible f)] : Field (AdjoinRoot f) where
   __ := instCommRing _
   __ := instGroupWithZero
+  qsmul := (· • ·)
   ratCast_def q := by
     rw [← map_natCast (of f), ← map_intCast (of f), ← map_div₀, ← Rat.cast_def]; rfl
-  qsmul := (· • ·)
   qsmul_def q x :=
     -- Porting note: I gave the explicit motive and changed `rw` to `simp`.
     AdjoinRoot.induction_on (C := fun y ↦ q • y = (of f) q * y) x fun p ↦ by
-      simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.rat_smul_eq_C_mul]
+      simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.qsmul_eq_C_mul]
 #align adjoin_root.field AdjoinRoot.instField
 
 theorem coe_injective (h : degree f ≠ 0) : Function.Injective ((↑) : K → AdjoinRoot f) :=
diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean
@@ -583,13 +583,11 @@ open FractionalIdeal
 
 open Ideal
 
-noncomputable instance FractionalIdeal.semifield : Semifield (FractionalIdeal A⁰ K) :=
-  { coeIdeal_injective.nontrivial with
-    inv := fun I => I⁻¹
-    inv_zero := inv_zero' _
-    div := (· / ·)
-    div_eq_mul_inv := FractionalIdeal.div_eq_mul_inv
-    mul_inv_cancel := fun I => FractionalIdeal.mul_inv_cancel }
+noncomputable instance FractionalIdeal.semifield : Semifield (FractionalIdeal A⁰ K) where
+  __ := coeIdeal_injective.nontrivial
+  inv_zero := inv_zero' _
+  div_eq_mul_inv := FractionalIdeal.div_eq_mul_inv
+  mul_inv_cancel _ := FractionalIdeal.mul_inv_cancel
 #align fractional_ideal.semifield FractionalIdeal.semifield
 
 /-- Fractional ideals have cancellative multiplication in a Dedekind domain.
diff --git a/Mathlib/RingTheory/HahnSeries/Summable.lean b/Mathlib/RingTheory/HahnSeries/Summable.lean
diff --git a/Mathlib/RingTheory/Ideal/Quotient.lean b/Mathlib/RingTheory/Ideal/Quotient.lean
diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean
diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
diff --git a/Mathlib/RingTheory/OreLocalization/Basic.lean b/Mathlib/RingTheory/OreLocalization/Basic.lean
diff --git a/Mathlib/RingTheory/SimpleModule.lean b/Mathlib/RingTheory/SimpleModule.lean
diff --git a/Mathlib/RingTheory/Subring/Basic.lean b/Mathlib/RingTheory/Subring/Basic.lean
diff --git a/Mathlib/Topology/Algebra/UniformField.lean b/Mathlib/Topology/Algebra/UniformField.lean
