refactor(data/is_R_or_C,analysis/inner_product_space): review API (#18919)

urkud · eric-wieser · urkud · commit 3f655f5297b0 · 2023-05-08T02:00:12.000Z
## Drop `is_R_or_C.abs` and lemmas about it

Use `has_norm.norm` instead. The norm is definitionally equal both to
`real.abs` and `complex.abs`, so it's easier to specialize generic
theorems to real numbers. Also, we don't have to convert between norm
and `is_R_or_C.abs` here and there.

- Drop `is_R_or_C.abs`, `is_R_or_C.norm_eq_abs`,
  `is_R_or_C.abs_of_nonneg`, `is_R_or_C.abs_zero`,
  `is_R_or_C.abs_one`, `is_R_or_C.abs_nonneg`,
  `is_R_or_C.abs_eq_zero`, `is_R_or_C.abs_ne_zero`,
  `is_R_or_C.abs_mul`, `is_R_or_C.abs_add`,
  `is_R_or_C.is_absolute_value`, `is_R_or_C.abs_abs`,
  `is_R_or_C.abs_pos`, `is_R_or_C.abs_neg`, `is_R_or_C.abs_inv`,
  `is_R_or_C.abs_div`, `is_R_or_C.abs_abs_sub_le_abs_sub`,
  `is_R_or_C.norm_sq_eq_abs`, `is_R_or_C.abs_to_real`,
  `is_R_or_C.continuous_abs`, `is_R_or_C.abs_to_complex`,
  `inner_product_space.core.abs_inner_symm`, `abs_inner_le_norm`.

## Rename/merge lemmas

### `is_R_or_C`

- Rename `is_R_or_C.of_real_smul` to `is_R_or_C.real_smul_of_real`.
- Merge `is_R_or_C.norm_real`, `is_R_or_C.norm_of_real`, and
  `is_R_or_C.abs_of_real` into `is_R_or_C.norm_of_real`.
- Merge `is_R_or_C.abs_of_nat` and `is_R_or_C.abs_cast_nat` into
  `is_R_or_C.norm_nat_cast`, use `has_norm.norm`, make it a `simp,
  priority 900, is_R_or_C_simps, norm_cast` lemma.
- Rename `is_R_or_C.mul_self_abs` to `is_R_or_C.mul_self_norm`, use
  `has_norm.norm`.
- Rename `is_R_or_C.abs_two` to `is_R_or_C.norm_two`, use
  `has_norm.norm`.
- Rename `is_R_or_C.abs_conj` to `is_R_or_C.norm_conj`, use
  `has_norm.norm`.
- Rename `is_R_or_C.abs_re_le_abs` to `is_R_or_C.abs_re_le_norm`, use
  `has_norm.norm`.
- Rename `is_R_or_C.abs_im_le_abs` to `is_R_or_C.abs_im_le_norm`, use
  `has_norm.norm`.
- Rename `is_R_or_C.re_le_abs` and `is_R_or_C.im_le_abs` to
  `is_R_or_C.re_le_norm` and `is_R_or_C.im_le_norm`, respectively; use
  `has_norm.norm`.
- Use `has_norm.norm` in `is_R_or_C.im_eq_zero_of_le` and
  `is_R_or_C.re_eq_self_of_le`.
- Rename `is_R_or_C.abs_re_div_abs_le_one` and
  `is_R_or_C.abs_im_div_abs_le_one` to
  `is_R_or_C.abs_re_div_norm_le_one` and
  `is_R_or_C.abs_im_div_norm_le_one`, respectively; use
  `has_norm.norm`.
- Rename `is_R_or_C.re_eq_abs_of_mul_conj` to
  `is_R_or_C.re_eq_norm_of_mul_conj`, use `has_norm.norm`.
- Rename `is_R_or_C.abs_sq_re_add_conj` and
  `is_R_or_C.abs_sq_re_add_conj'` to `is_R_or_C.norm_sq_re_add_conj`
  and `is_R_or_C.norm_sq_re_conj_add`, respectively; use
  `has_norm.norm`.
- Use `has_norm.norm` in all lemmas/definitions about `is_cau_seq` and
  `cau_seq` sequences of `is_R_or_C` numbers.
- Rename `is_R_or_C.is_cau_seq_abs` to `is_R_or_C.is_cau_seq_norm`,
  use `has_norm.norm`.

### Inner products

- Rename `inner_product_space.core.inner_mul_conj_re_abs` to
  `inner_product_space.core.inner_mul_symm_re_eq_norm`, use
  `has_norm.norm`.
- Do the same in the root NS.
- Rename `inner_self_re_abs` to `inner_self_re_eq_norm`, use
  `has_norm.norm`.
- Rename `inner_self_abs_to_K` to `inner_self_norm_to_K`, use
  `has_norm.norm`.
- Rename `abs_inner_symm` to `norm_inner_symm`, use `has_norm.norm`.
- Rename
  `abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul` to
  `norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul`, use
  `has_norm.norm`.

## Add lemmas

- Add `is_R_or_C.is_real_tfae` and `is_real_tfae.conj_eq_iff_im`.
- Add `is_R_or_C.norm_sq_apply`.


## Change attributes

- `is_R_or_C.zero_re'` is no longer a `simp` lemma
- `is_R_or_C.norm_conj` is now a `simp` lemma.

## Misc

- Reorder lemmas here and there to golf.



Co-authored-by: Eric Wieser &lt;wieser.eric@gmail.com&gt;
diff --git a/docs/100.yaml b/docs/100.yaml
@@ -315,7 +315,7 @@
   title  : The Cauchy-Schwarz Inequality
   decls  :
     - inner_mul_inner_self_le
-    - abs_inner_le_norm
+    - norm_inner_le_norm
   author : Zhouhang Zhou
 79:
   title  : The Intermediate Value Theorem
diff --git a/src/analysis/calculus/uniform_limits_deriv.lean b/src/analysis/calculus/uniform_limits_deriv.lean
@@ -349,8 +349,8 @@ begin
   --   * The `f' n` converge to `g'` at `x`
   conv
   { congr, funext,
-    rw [←norm_norm, ←norm_inv,←@is_R_or_C.norm_of_real 𝕜 _ _,
-      is_R_or_C.of_real_inv, ←norm_smul], },
+    rw [← abs_norm, ← abs_inv, ← @is_R_or_C.norm_of_real 𝕜 _ _,
+      is_R_or_C.of_real_inv, ← norm_smul], },
   rw ←tendsto_zero_iff_norm_tendsto_zero,
   have : (λ a : ι × E, (‖a.2 - x‖⁻¹ : 𝕜) • (g a.2 - g x - (g' x) (a.2 - x))) =
     (λ a : ι × E, (‖a.2 - x‖⁻¹ : 𝕜) • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) +
diff --git a/src/analysis/complex/basic.lean b/src/analysis/complex/basic.lean
@@ -321,7 +321,7 @@ section complex_order
 open_locale complex_order
 
 lemma eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) : z = ↑‖z‖ :=
-by rw [eq_re_of_real_le hz, is_R_or_C.norm_of_real, real.norm_of_nonneg (complex.le_def.2 hz).1]
+by rw [eq_re_of_real_le hz, is_R_or_C.norm_of_real, _root_.abs_of_nonneg (complex.le_def.2 hz).1]
 
 end complex_order
 
@@ -334,16 +334,12 @@ open_locale complex_conjugate
 local notation `reC` := @is_R_or_C.re ℂ _
 local notation `imC` := @is_R_or_C.im ℂ _
 local notation `IC` := @is_R_or_C.I ℂ _
-local notation `absC` := @is_R_or_C.abs ℂ _
 local notation `norm_sqC` := @is_R_or_C.norm_sq ℂ _
 
 @[simp] lemma re_to_complex {x : ℂ} : reC x = x.re := rfl
 @[simp] lemma im_to_complex {x : ℂ} : imC x = x.im := rfl
 @[simp] lemma I_to_complex : IC = complex.I := rfl
-@[simp] lemma norm_sq_to_complex {x : ℂ} : norm_sqC x = complex.norm_sq x :=
-by simp [is_R_or_C.norm_sq, complex.norm_sq]
-@[simp] lemma abs_to_complex {x : ℂ} : absC x = complex.abs x :=
-by simp [is_R_or_C.abs, complex.abs]
+@[simp] lemma norm_sq_to_complex {x : ℂ} : norm_sqC x = complex.norm_sq x := rfl
 
 section tsum
 variables {α : Type*} (𝕜 : Type*) [is_R_or_C 𝕜]
diff --git a/src/analysis/complex/schwarz.lean b/src/analysis/complex/schwarz.lean
@@ -98,7 +98,7 @@ begin
   have hg₀ : ‖g‖₊ ≠ 0, by simpa only [hg'] using one_ne_zero,
   calc ‖dslope f c z‖ = ‖dslope (g ∘ f) c z‖ :
     begin
-      rw [g.dslope_comp, hgf, is_R_or_C.norm_of_real, norm_norm],
+      rw [g.dslope_comp, hgf, is_R_or_C.norm_of_real, abs_norm],
       exact λ _, hd.differentiable_at (ball_mem_nhds _ hR₁)
     end
   ... ≤ R₂ / R₁ :
diff --git a/src/analysis/convex/gauge.lean b/src/analysis/convex/gauge.lean
@@ -290,13 +290,11 @@ variables [is_R_or_C 𝕜] [module 𝕜 E] [is_scalar_tower ℝ 𝕜 E]
 
 lemma gauge_norm_smul (hs : balanced 𝕜 s) (r : 𝕜) (x : E) : gauge s (‖r‖ • x) = gauge s (r • x) :=
 begin
-  rw @is_R_or_C.real_smul_eq_coe_smul 𝕜,
-  obtain rfl | hr := eq_or_ne r 0,
-  { simp only [norm_zero, is_R_or_C.of_real_zero] },
   unfold gauge,
   congr' with θ,
+  rw @is_R_or_C.real_smul_eq_coe_smul 𝕜,
   refine and_congr_right (λ hθ, (hs.smul _).mem_smul_iff _),
-  rw [is_R_or_C.norm_of_real, norm_norm],
+  rw [is_R_or_C.norm_of_real, abs_norm],
 end
 
 /-- If `s` is balanced, then the Minkowski functional is ℂ-homogeneous. -/
diff --git a/src/analysis/inner_product_space/basic.lean b/src/analysis/inner_product_space/basic.lean
@@ -154,7 +154,6 @@ include c
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 F _ x y
 local notation `norm_sqK` := @is_R_or_C.norm_sq 𝕜 _
 local notation `reK` := @is_R_or_C.re 𝕜 _
-local notation `absK` := @is_R_or_C.abs 𝕜 _
 local notation `ext_iff` := @is_R_or_C.ext_iff 𝕜 _
 local postfix `†`:90 := star_ring_end _
 
@@ -219,11 +218,8 @@ inner_self_eq_zero.not
 lemma inner_self_re_to_K (x : F) : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
 by norm_num [ext_iff, inner_self_im]
 
-lemma abs_inner_symm (x y : F) : abs ⟪x, y⟫ = abs ⟪y, x⟫ :=
-by rw [←inner_conj_symm, abs_conj]
-
 lemma norm_inner_symm (x y : F) : ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖ :=
-by rw [is_R_or_C.norm_eq_abs, is_R_or_C.norm_eq_abs, abs_inner_symm]
+by rw [←inner_conj_symm, norm_conj]
 
 lemma inner_neg_left (x y : F) : ⟪-x, y⟫ = -⟪x, y⟫ :=
 by { rw [← neg_one_smul 𝕜 x, inner_smul_left], simp }
@@ -237,8 +233,8 @@ by { simp [sub_eq_add_neg, inner_add_left, inner_neg_left] }
 lemma inner_sub_right (x y z : F) : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫ :=
 by { simp [sub_eq_add_neg, inner_add_right, inner_neg_right] }
 
-lemma inner_mul_conj_re_abs (x y : F) : re (⟪x, y⟫ * ⟪y, x⟫) = abs (⟪x, y⟫ * ⟪y, x⟫) :=
-by { rw [←inner_conj_symm, mul_comm], exact re_eq_abs_of_mul_conj (inner y x), }
+lemma inner_mul_symm_re_eq_norm (x y : F) : re (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖ :=
+by { rw [←inner_conj_symm, mul_comm], exact re_eq_norm_of_mul_conj (inner y x), }
 
 /-- Expand `inner (x + y) (x + y)` -/
 lemma inner_add_add_self (x y : F) : ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ :=
@@ -310,7 +306,7 @@ add_group_norm.to_normed_add_comm_group
   neg' := λ x, by simp only [inner_neg_left, neg_neg, inner_neg_right],
   add_le' := λ x y, begin
     have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ := norm_inner_le_norm _ _,
-    have h₂ : re ⟪x, y⟫ ≤ ‖⟪x, y⟫‖ := (re_le_abs _).trans_eq (is_R_or_C.norm_eq_abs _).symm,
+    have h₂ : re ⟪x, y⟫ ≤ ‖⟪x, y⟫‖ := re_le_norm _,
     have h₃ : re ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ := h₂.trans h₁,
     have h₄ : re ⟪y, x⟫ ≤ ‖x‖ * ‖y‖ := by rwa [←inner_conj_symm, conj_re],
     have : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖),
@@ -362,8 +358,6 @@ variables [normed_add_comm_group F] [inner_product_space ℝ F]
 variables [dec_E : decidable_eq E]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 local notation `IK` := @is_R_or_C.I 𝕜 _
-local notation `absR` := has_abs.abs
-local notation `absK` := @is_R_or_C.abs 𝕜 _
 local postfix `†`:90 := star_ring_end _
 
 export inner_product_space (norm_sq_eq_inner)
@@ -478,20 +472,23 @@ inner_product_space.to_core.nonneg_re x
 lemma real_inner_self_nonneg {x : F} : 0 ≤ ⟪x, x⟫_ℝ := @inner_self_nonneg ℝ F _ _ _ x
 
 @[simp] lemma inner_self_re_to_K (x : E) : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
-is_R_or_C.ext_iff.2 ⟨by simp only [of_real_re], by simp only [inner_self_im, of_real_im]⟩
+((is_R_or_C.is_real_tfae (⟪x, x⟫ : 𝕜)).out 2 3).2 (inner_self_im _)
 
 lemma inner_self_eq_norm_sq_to_K (x : E) : ⟪x, x⟫ = (‖x‖ ^ 2 : 𝕜) :=
 by rw [← inner_self_re_to_K, ← norm_sq_eq_inner, of_real_pow]
 
-lemma inner_self_re_abs (x : E) : re ⟪x, x⟫ = abs ⟪x, x⟫ :=
+lemma inner_self_re_eq_norm (x : E) : re ⟪x, x⟫ = ‖⟪x, x⟫‖ :=
 begin
   conv_rhs { rw [←inner_self_re_to_K] },
   symmetry,
-  exact is_R_or_C.abs_of_nonneg inner_self_nonneg,
+  exact norm_of_nonneg inner_self_nonneg,
 end
 
-lemma inner_self_abs_to_K (x : E) : (absK ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
-by { rw [←inner_self_re_abs], exact inner_self_re_to_K _ }
+lemma inner_self_norm_to_K (x : E) : (‖⟪x, x⟫‖ : 𝕜) = ⟪x, x⟫ :=
+by { rw [←inner_self_re_eq_norm], exact inner_self_re_to_K _ }
+
+lemma real_inner_self_abs (x : F) : |⟪x, x⟫_ℝ| = ⟪x, x⟫_ℝ :=
+@inner_self_norm_to_K ℝ F _ _ _ x
 
 @[simp] lemma inner_self_eq_zero {x : E} : ⟪x, x⟫ = 0 ↔ x = 0 :=
 by rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, of_real_eq_zero, norm_eq_zero]
@@ -505,11 +502,8 @@ by rw [← norm_sq_eq_inner, (sq_nonneg _).le_iff_eq, sq_eq_zero_iff, norm_eq_ze
 lemma real_inner_self_nonpos {x : F} : ⟪x, x⟫_ℝ ≤ 0 ↔ x = 0 :=
 @inner_self_nonpos ℝ F _ _ _ x
 
-lemma real_inner_self_abs (x : F) : absR ⟪x, x⟫_ℝ = ⟪x, x⟫_ℝ :=
-by { have h := @inner_self_abs_to_K ℝ F _ _ _ x, simpa using h }
-
-lemma abs_inner_symm (x y : E) : abs ⟪x, y⟫ = abs ⟪y, x⟫ :=
-by rw [←inner_conj_symm, abs_conj]
+lemma norm_inner_symm (x y : E) : ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖ :=
+by rw [←inner_conj_symm, norm_conj]
 
 @[simp] lemma inner_neg_left (x y : E) : ⟪-x, y⟫ = -⟪x, y⟫ :=
 by { rw [← neg_one_smul 𝕜 x, inner_smul_left], simp }
@@ -528,8 +522,8 @@ by { simp [sub_eq_add_neg, inner_add_left] }
 lemma inner_sub_right (x y z : E) : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫ :=
 by { simp [sub_eq_add_neg, inner_add_right] }
 
-lemma inner_mul_conj_re_abs (x y : E) : re (⟪x, y⟫ * ⟪y, x⟫) = abs (⟪x, y⟫ * ⟪y, x⟫) :=
-by { rw [←inner_conj_symm, mul_comm], exact re_eq_abs_of_mul_conj (inner y x), }
+lemma inner_mul_symm_re_eq_norm (x y : E) : re (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖ :=
+by { rw [←inner_conj_symm, mul_comm], exact re_eq_norm_of_mul_conj (inner y x), }
 
 /-- Expand `⟪x + y, x + y⟫` -/
 lemma inner_add_add_self (x y : E) : ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ :=
@@ -939,14 +933,11 @@ begin
   exact inner_product_space.core.norm_inner_le_norm x y
 end
 
-lemma abs_inner_le_norm (x y : E) : abs ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ :=
-(norm_eq_abs ⟪x, y⟫).symm.trans_le (norm_inner_le_norm _ _)
-
 lemma nnnorm_inner_le_nnnorm (x y : E) : ‖⟪x, y⟫‖₊ ≤ ‖x‖₊ * ‖y‖₊ :=
 norm_inner_le_norm x y
 
 lemma re_inner_le_norm (x y : E) : re ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ :=
-le_trans (re_le_abs (inner x y)) (abs_inner_le_norm x y)
+le_trans (re_le_norm (inner x y)) (norm_inner_le_norm x y)
 
 /-- Cauchy–Schwarz inequality with norm -/
 lemma abs_real_inner_le_norm (x y : F) : |⟪x, y⟫_ℝ| ≤ ‖x‖ * ‖y‖ :=
@@ -1322,9 +1313,9 @@ end
 
 /-- The real inner product of two vectors, divided by the product of their
 norms, has absolute value at most 1. -/
-lemma abs_real_inner_div_norm_mul_norm_le_one (x y : F) : absR (⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)) ≤ 1 :=
+lemma abs_real_inner_div_norm_mul_norm_le_one (x y : F) : |⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| ≤ 1 :=
 begin
-  rw [_root_.abs_div, _root_.abs_mul, abs_norm, abs_norm],
+  rw [abs_div, abs_mul, abs_norm, abs_norm],
   exact div_le_one_of_le (abs_real_inner_le_norm x y) (by positivity)
 end
 
@@ -1339,36 +1330,31 @@ by rw [inner_smul_right, ←real_inner_self_eq_norm_mul_norm]
 /-- The inner product of a nonzero vector with a nonzero multiple of
 itself, divided by the product of their norms, has absolute value
 1. -/
-lemma abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul
-  {x : E} {r : 𝕜} (hx : x ≠ 0) (hr : r ≠ 0) : abs ⟪x, r • x⟫ / (‖x‖ * ‖r • x‖) = 1 :=
+lemma norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul
+  {x : E} {r : 𝕜} (hx : x ≠ 0) (hr : r ≠ 0) : ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1 :=
 begin
-  have hx' : ‖x‖ ≠ 0 := by simp [norm_eq_zero, hx],
-  have hr' : abs r ≠ 0 := by simp [is_R_or_C.abs_eq_zero, hr],
-  rw [inner_smul_right, is_R_or_C.abs_mul, ←inner_self_re_abs, inner_self_eq_norm_mul_norm,
-      norm_smul],
-  rw [is_R_or_C.norm_eq_abs, ←mul_assoc, ←div_div, mul_div_cancel _ hx',
-     ←div_div, mul_comm, mul_div_cancel _ hr', div_self hx'],
+  have hx' : ‖x‖ ≠ 0 := by simp [hx],
+  have hr' : ‖r‖ ≠ 0 := by simp [hr],
+  rw [inner_smul_right, norm_mul, ← inner_self_re_eq_norm, inner_self_eq_norm_mul_norm, norm_smul],
+  rw [← mul_assoc, ← div_div, mul_div_cancel _ hx',
+     ← div_div, mul_comm, mul_div_cancel _ hr', div_self hx'],
 end
 
 /-- The inner product of a nonzero vector with a nonzero multiple of
 itself, divided by the product of their norms, has absolute value
 1. -/
 lemma abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul
-  {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r ≠ 0) : absR ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1 :=
-begin
-  rw ← abs_to_real,
-  exact abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr
-end
+  {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r ≠ 0) : |⟪x, r • x⟫_ℝ| / (‖x‖ * ‖r • x‖) = 1 :=
+norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr
 
 /-- The inner product of a nonzero vector with a positive multiple of
 itself, divided by the product of their norms, has value 1. -/
 lemma real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul
   {x : F} {r : ℝ} (hx : x ≠ 0) (hr : 0 < r) : ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1 :=
 begin
-  rw [real_inner_smul_self_right, norm_smul, real.norm_eq_abs, ←mul_assoc ‖x‖, mul_comm _ (absR r),
-      mul_assoc, _root_.abs_of_nonneg (le_of_lt hr), div_self],
-  exact mul_ne_zero (ne_of_gt hr)
-    (λ h, hx (norm_eq_zero.1 (eq_zero_of_mul_self_eq_zero h)))
+  rw [real_inner_smul_self_right, norm_smul, real.norm_eq_abs, ←mul_assoc ‖x‖, mul_comm _ (|r|),
+      mul_assoc, abs_of_nonneg hr.le, div_self],
+  exact mul_ne_zero hr.ne' (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))
 end
 
 /-- The inner product of a nonzero vector with a negative multiple of
@@ -1431,9 +1417,8 @@ begin
     refine ⟨hx₀, (norm_inner_eq_norm_iff hx₀ hy₀).1 $ eq_of_div_eq_one _⟩,
     simpa using h },
   { rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩,
-    simp only [is_R_or_C.abs_div, is_R_or_C.abs_mul, is_R_or_C.abs_of_real, is_R_or_C.norm_eq_abs,
-      abs_norm],
-    exact abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr }
+    simp only [norm_div, norm_mul, norm_of_real, abs_norm],
+    exact norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr }
 end
 
 /-- The inner product of two vectors, divided by the product of their
@@ -1452,7 +1437,7 @@ begin
   { have : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫ : 𝕜) • x :=
       ((@norm_inner_eq_norm_tfae 𝕜 _ _ _ _ x y).out 0 1).1 (by simp [h]),
     rw [this.resolve_left h₀, h],
-    simp [norm_smul, is_R_or_C.norm_eq_abs, inner_self_abs_to_K, h₀'] },
+    simp [norm_smul, inner_self_norm_to_K, h₀'] },
   { conv_lhs { rw [← h, inner_smul_right, inner_self_eq_norm_sq_to_K] },
     field_simp [sq, mul_left_comm] }
 end
@@ -1569,7 +1554,7 @@ begin
   { simp },
   { refine (mul_le_mul_right (norm_pos_iff.2 h)).mp _,
     calc ‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ : by rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow,
-      norm_of_real, norm_norm]
+      norm_of_real, abs_norm]
     ... ≤ ‖innerSL 𝕜 x‖ * ‖x‖ : (innerSL 𝕜 x).le_op_norm _ }
 end
 
@@ -1867,12 +1852,12 @@ begin
     use a,
     intros s₁ hs₁ s₂ hs₂,
     rw ← finset.sum_sdiff_sub_sum_sdiff,
-    refine (_root_.abs_sub _ _).trans_lt _,
+    refine (abs_sub _ _).trans_lt _,
     have : ∀ i, 0 ≤ ‖f i‖ ^ 2 := λ i : ι, sq_nonneg _,
     simp only [finset.abs_sum_of_nonneg' this],
     have : ∑ i in s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i in s₂ \ s₁, ‖f i‖ ^ 2 < (sqrt ε) ^ 2,
-    { rw [← hV.norm_sq_diff_sum, sq_lt_sq,
-        _root_.abs_of_nonneg (sqrt_nonneg _), _root_.abs_of_nonneg (norm_nonneg _)],
+    { rw [← hV.norm_sq_diff_sum, sq_lt_sq, abs_of_nonneg (sqrt_nonneg _),
+        abs_of_nonneg (norm_nonneg _)],
       exact H s₁ hs₁ s₂ hs₂ },
     have hη := sq_sqrt (le_of_lt hε),
     linarith },
diff --git a/src/analysis/inner_product_space/rayleigh.lean b/src/analysis/inner_product_space/rayleigh.lean
@@ -67,7 +67,7 @@ begin
     let c : 𝕜 := ↑‖x‖⁻¹ * r,
     have : c ≠ 0 := by simp [c, hx, hr.ne'],
     refine ⟨c • x, _, _⟩,
-    { field_simp [norm_smul, is_R_or_C.norm_eq_abs, abs_of_nonneg hr.le] },
+    { field_simp [norm_smul, abs_of_pos hr] },
     { rw T.rayleigh_smul x this,
       exact hxT } },
   { rintros ⟨x, hx, hxT⟩,
diff --git a/src/analysis/inner_product_space/symmetric.lean b/src/analysis/inner_product_space/symmetric.lean
@@ -166,7 +166,7 @@ begin
       inner_add_right, inner_sub_left, inner_sub_right, hT x, ← inner_conj_symm x (T y)],
     suffices : (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫,
     { rw conj_eq_iff_re.mpr this,
-      ring_nf, },
+      ring, },
     { rw ← re_add_im ⟪T y, x⟫,
       simp_rw [h, mul_zero, add_zero],
       norm_cast, } },
diff --git a/src/analysis/locally_convex/continuous_of_bounded.lean b/src/analysis/locally_convex/continuous_of_bounded.lean
@@ -108,10 +108,9 @@ begin
       rw ←hy,
       refine (bE1 (n+1)).2.smul_mem  _ hx,
       have h' : 0 < (n : ℝ) + 1 := n.cast_add_one_pos,
-      rw [norm_inv, ←nat.cast_one, ←nat.cast_add, is_R_or_C.norm_eq_abs, is_R_or_C.abs_cast_nat,
-        nat.cast_add, nat.cast_one, inv_le h' zero_lt_one],
-      norm_cast,
-      simp, },
+      rw [norm_inv, ←nat.cast_one, ←nat.cast_add, is_R_or_C.norm_nat_cast, nat.cast_add,
+        nat.cast_one, inv_le h' zero_lt_one],
+      simp },
     intros n hn,
     -- The converse direction follows from continuity of the scalar multiplication
     have hcont : continuous_at (λ (x : E), (n : 𝕜) • x) 0 :=
@@ -149,7 +148,7 @@ begin
   cases exists_nat_gt r with n hn,
   -- We now find a contradiction between `f (u n) ∉ V` and the absorbing property
   have h1 : r ≤ ‖(n : 𝕜')‖ :=
-  by { rw [is_R_or_C.norm_eq_abs, is_R_or_C.abs_cast_nat], exact hn.le },
+  by { rw [is_R_or_C.norm_nat_cast], exact hn.le },
   have hn' : 0 < ‖(n : 𝕜')‖ := lt_of_lt_of_le hr h1,
   rw [norm_pos_iff, ne.def, nat.cast_eq_zero] at hn',
   have h'' : f (u n) ∈ V :=
diff --git a/src/analysis/normed_space/exponential.lean b/src/analysis/normed_space/exponential.lean
@@ -367,7 +367,7 @@ begin
   refine summable_of_norm_bounded_eventually _ (real.summable_pow_div_factorial r) _,
   filter_upwards [eventually_cofinite_ne 0] with n hn,
   rw [norm_mul, norm_norm (exp_series 𝕂 𝔸 n), exp_series, norm_smul, norm_inv, norm_pow,
-      nnreal.norm_eq, norm_eq_abs, abs_cast_nat, mul_comm, ←mul_assoc, ←div_eq_mul_inv],
+      nnreal.norm_eq, norm_nat_cast, mul_comm, ←mul_assoc, ←div_eq_mul_inv],
   have : ‖continuous_multilinear_map.mk_pi_algebra_fin 𝕂 n 𝔸‖ ≤ 1 :=
     norm_mk_pi_algebra_fin_le_of_pos (nat.pos_of_ne_zero hn),
   exact mul_le_of_le_one_right (div_nonneg (pow_nonneg r.coe_nonneg n) n!.cast_nonneg) this
diff --git a/src/analysis/normed_space/extend.lean b/src/analysis/normed_space/extend.lean
@@ -122,7 +122,7 @@ lemma extend_to_𝕜'_apply (fr : F →L[ℝ] ℝ) (x : F) :
 le_antisymm (linear_map.mk_continuous_norm_le _ (norm_nonneg _) _) $
   op_norm_le_bound _ (norm_nonneg _) $ λ x,
     calc ‖fr x‖ = ‖re (fr.extend_to_𝕜' x : 𝕜)‖ : congr_arg norm (fr.extend_to_𝕜'_apply_re x).symm
-    ... ≤ ‖(fr.extend_to_𝕜' x : 𝕜)‖ : (abs_re_le_abs _).trans_eq (norm_eq_abs _).symm
+    ... ≤ ‖(fr.extend_to_𝕜' x : 𝕜)‖ : abs_re_le_norm _
     ... ≤ ‖(fr.extend_to_𝕜' : F →L[𝕜] 𝕜)‖ * ‖x‖ : le_op_norm _ _
 
 end continuous_linear_map
diff --git a/src/analysis/normed_space/is_R_or_C.lean b/src/analysis/normed_space/is_R_or_C.lean
@@ -46,7 +46,7 @@ lemma norm_smul_inv_norm' {r : ℝ} (r_nonneg : 0 ≤ r) {x : E} (hx : x ≠ 0)
   ‖(r * ‖x‖⁻¹ : 𝕜) • x‖ = r :=
 begin
   have : ‖x‖ ≠ 0 := by simp [hx],
-  field_simp [norm_smul, is_R_or_C.norm_eq_abs, r_nonneg] with is_R_or_C_simps
+  field_simp [norm_smul, r_nonneg] with is_R_or_C_simps
 end
 
 lemma linear_map.bound_of_sphere_bound
diff --git a/src/analysis/normed_space/spectrum.lean b/src/analysis/normed_space/spectrum.lean
@@ -478,8 +478,7 @@ begin
   have hb : summable (λ n : ℕ, ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐz) ^ n),
   { refine summable_of_norm_bounded_eventually _ (real.summable_pow_div_factorial ‖a - ↑ₐz‖) _,
     filter_upwards [filter.eventually_cofinite_ne 0] with n hn,
-    rw [norm_smul, mul_comm, norm_inv, is_R_or_C.norm_eq_abs, is_R_or_C.abs_cast_nat,
-      ←div_eq_mul_inv],
+    rw [norm_smul, mul_comm, norm_inv, is_R_or_C.norm_nat_cast, ← div_eq_mul_inv],
     exact div_le_div (pow_nonneg (norm_nonneg _) n) (norm_pow_le' (a - ↑ₐz) (zero_lt_iff.mpr hn))
       (by exact_mod_cast nat.factorial_pos n)
       (by exact_mod_cast nat.factorial_le (lt_add_one n).le) },
diff --git a/src/data/is_R_or_C/basic.lean b/src/data/is_R_or_C/basic.lean
diff --git a/src/measure_theory/function/l2_space.lean b/src/measure_theory/function/l2_space.lean
diff --git a/src/ring_theory/polynomial/cyclotomic/eval.lean b/src/ring_theory/polynomial/cyclotomic/eval.lean
