chore: Final cleanup before NNRat.cast (#12360)

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 _` to make the instances more robust to definition changes.
* Delete `qsmulRec`.
* Move `qsmul` before `ratCast_def` in instance declarations.
* Name more instances.
* Rename `rat_smul` to `qsmul`.

Author: YaelDillies

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

Mathlib/Algebra/Field/Defs.lean

@@ -68,15 +68,7 @@ better definitional properties). Instead, use the coercion. -/
 def Rat.castRec [NatCast K] [IntCast K] [Div K] (q : ℚ) : K := q.num / q.den
 #align rat.cast_rec Rat.castRec
 
-/-- The default definition of the scalar multiplication by `ℚ` on a division ring `K`.
-
-`q • x` is defined as `↑q * x`.
-
-Do not use directly (instances of `DivisionRing` are allowed to override that default for
-better definitional properties). Instead use the `•` notation. -/
-def qsmulRec (coe : ℚ → K) [Mul K] (a : ℚ) (x : K) : K :=
-  coe a * x
-#align qsmul_rec qsmulRec
+#noalign qsmul_rec
 
 /-- A `DivisionSemiring` is a `Semiring` with multiplicative inverses for nonzero elements.
 
@@ -113,7 +105,8 @@ class DivisionRing (α : Type*)
   protected ratCast_def (q : ℚ) : (Rat.cast q : α) = q.num / q.den := by intros; rfl
   /-- Scalar multiplication by a rational number.
 
-  Set this to `qsmulRec _` unless there is a risk of a `Module ℚ _` instance diamond.
+  Unless there is a risk of a `Module ℚ _` instance diamond, write `qsmul := _`. This will set
+  `qsmul` to `(Rat.cast · * ·)` thanks to unification in the default proof of `qsmul_def`.
 
   Do not use directly. Instead use the `•` notation. -/
   protected qsmul : ℚ → α → α

Mathlib/Algebra/Field/IsField.lean

@@ -63,18 +63,17 @@ 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`. -/
 noncomputable def IsField.toField {R : Type u} [Ring R] (h : IsField R) : Field R :=
-  { ‹Ring R›, IsField.toSemifield h with qsmul := qsmulRec _ }
+  { ‹Ring R›, IsField.toSemifield h with qsmul := _ }
 #align is_field.to_field IsField.toField
 
 /-- For each field, and for each nonzero element of said field, there is a unique inverse.

Mathlib/Algebra/Field/MinimalAxioms.lean

@@ -42,4 +42,4 @@ def Field.ofMinimalAxioms (K : Type u)
   { exists_pair_ne := exists_pair_ne
     mul_inv_cancel := mul_inv_cancel
     inv_zero := inv_zero
-    qsmul := qsmulRec _ }
+    qsmul := _ }

Mathlib/Algebra/Field/Opposite.lean

@@ -38,9 +38,9 @@ instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵐᵒ
 instance instDivisionRing [DivisionRing α] : DivisionRing αᵐᵒᵖ where
   __ := instRing
   __ := instDivisionSemiring
+  qsmul := _
   ratCast_def q := unop_injective <| by rw [unop_ratCast, Rat.cast_def, unop_div,
     unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
-  qsmul := qsmulRec _
 
 instance instSemifield [Semifield α] : Semifield αᵐᵒᵖ where
   __ := instCommSemiring
@@ -61,9 +61,9 @@ instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵃᵒ
 instance instDivisionRing [DivisionRing α] : DivisionRing αᵃᵒᵖ where
   __ := instRing
   __ := instDivisionSemiring
+  qsmul := _
   ratCast_def q := unop_injective <| by rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
     unop_intCast, div_eq_mul_inv]
-  qsmul := qsmulRec _
 
 instance instSemifield [Semifield α] : Semifield αᵃᵒᵖ where
   __ := instCommSemiring

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 α) where ratCast q := up q
 
-@[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

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.

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
 

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
 

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