perf(Algebra/Ring): faster Ring.toAddGroupWithOne instance

Mathlib/Algebra/Field/Defs.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Ring.Defs
 public import Mathlib.Data.Rat.Init
+public import Mathlib.Tactic.FastInstance
 
 /-!
 # Division (semi)rings and (semi)fields
@@ -180,7 +181,8 @@ If the field has positive characteristic `p`, our division by zero convention fo
 class Field (K : Type u) extends CommRing K, DivisionRing K
 
 -- see Note [lower instance priority]
-instance (priority := 100) Field.toSemifield [Field K] : Semifield K := { ‹Field K› with }
+instance (priority := 100) Field.toSemifield [Field K] : Semifield K :=
+  fast_instance% { ‹Field K› with }
 
 namespace NNRat
 variable [DivisionSemiring K]

Mathlib/Algebra/Ring/Defs.lean

@@ -145,6 +145,13 @@ class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α,
 /-- A `Ring` is a `Semiring` with negation making it an additive group. -/
 class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
 
+attribute [-instance] Ring.toAddGroupWithOne
+
+instance Ring.toAddGroupWithOne' (R : Type u) [Ring R] : AddGroupWithOne R :=
+  @AddGroupWithOne.mk R Ring.toIntCast inferInstance inferInstance
+    inferInstance Ring.sub_eq_add_neg Ring.zsmul Ring.zsmul_zero' Ring.zsmul_succ'
+    Ring.zsmul_neg' Ring.neg_add_cancel intCast_ofNat intCast_negSucc
+
 /-!
 ### Semirings
 -/

Mathlib/Analysis/RCLike/Basic.lean

@@ -674,10 +674,6 @@ variable (K) in
 lemma nnnorm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖₊ = q • ‖x‖₊ := by
   simpa [NNRat.cast_smul_eq_nnqsmul] using nnnorm_smul (q : K) x
 
-@[bound]
-lemma norm_expect_le {ι : Type*} {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=
-  Finset.le_expect_of_subadditive norm_zero norm_add_le fun _ _ ↦ by rw [norm_nnqsmul K]
-
 end NormedField
 
 theorem mul_self_norm (z : K) : ‖z‖ * ‖z‖ = normSq z := by rw [normSq_eq_def', sq]
@@ -788,6 +784,11 @@ end Instances
 
 namespace RCLike
 
+@[bound]
+lemma norm_expect_le {K : Type*} {E : Type*} [RCLike K] [NormedField E] [CharZero E]
+    [NormedSpace K E] {ι : Type u_3} {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=
+  Finset.le_expect_of_subadditive norm_zero norm_add_le fun _ _ ↦ by rw [norm_nnqsmul K]
+
 section Order
 
 open scoped ComplexOrder