chore(analysis/normed_space/basic): rename abs_norm_eq_norm to `abs…

…_norm` (#18921)

src/analysis/complex/open_mapping.lean

@@ -140,7 +140,7 @@ begin
       simpa [gray, ray] using h w e2 },
     have h4 : ‖z - z₀‖ < r := by simpa [dist_eq_norm] using mem_ball.mp hz,
     replace h4 : ↑‖z - z₀‖ ∈ ball (0 : ℂ) r := by simpa only [mem_ball_zero_iff, norm_eq_abs,
-      abs_of_real, abs_norm_eq_norm],
+      abs_of_real, abs_norm],
     simpa only [gray, ray, smul_smul, mul_inv_cancel h', one_smul, add_sub_cancel'_right,
       function.comp_app, coe_smul] using h3 ↑‖z - z₀‖ h4 },
   { right, -- Otherwise, it is open along at least one direction and that implies the result

src/analysis/inner_product_space/basic.lean

@@ -1519,7 +1519,7 @@ begin
         is_R_or_C.abs_div, is_R_or_C.abs_mul, ←inner_self_re_abs,
         inner_self_eq_norm_mul_norm] at h,
       norm_cast at h,
-      rwa [_root_.abs_mul, abs_norm_eq_norm, abs_norm_eq_norm, ←mul_assoc, mul_comm,
+      rwa [_root_.abs_mul, abs_norm, abs_norm, ←mul_assoc, mul_comm,
         mul_div_mul_left _ _ (λ h, hx0 (norm_eq_zero.1 h)), ←is_R_or_C.norm_eq_abs,
         ←norm_smul] at h },
     have hr0 : r ≠ 0,
@@ -1544,7 +1544,7 @@ begin
     rcases h with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩,
     rw [hy, is_R_or_C.abs_div],
     norm_cast,
-    rw [_root_.abs_mul, abs_norm_eq_norm, abs_norm_eq_norm],
+    rw [_root_.abs_mul, abs_norm, abs_norm],
     exact abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr }
 end
 
@@ -1648,7 +1648,7 @@ begin
   ... ↔ ‖(‖y‖:𝕜) • x - (‖x‖:𝕜) • y‖ * ‖(‖y‖:𝕜) • x - (‖x‖:𝕜) • y‖ = 0 :
   begin
     simp only [@norm_sub_mul_self 𝕜, inner_smul_left, inner_smul_right, norm_smul, conj_of_real,
-      is_R_or_C.norm_eq_abs, abs_of_real, of_real_im, of_real_re, mul_re, abs_norm_eq_norm],
+      is_R_or_C.norm_eq_abs, abs_of_real, of_real_im, of_real_re, mul_re, abs_norm],
     refine eq.congr _ rfl,
     ring
   end

src/analysis/inner_product_space/calculus.lean

@@ -364,7 +364,7 @@ begin
     refl, },
   refine cont_diff_at.congr_of_eventually_eq _ hf,
   suffices : cont_diff_at ℝ n (λy, (1 - ‖(y : E)‖^2).sqrt⁻¹) y, { exact this.smul cont_diff_at_id },
-  have h : 0 < 1 - ‖(y : E)‖^2, by rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm_eq_norm,
+  have h : 0 < 1 - ‖(y : E)‖^2, by rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm,
     ← sq_lt_sq, one_pow, ← sub_pos] at hy,
   refine cont_diff_at.inv _ (real.sqrt_ne_zero'.mpr h),
   refine cont_diff_at.comp _ (cont_diff_at_sqrt h.ne.symm) _,

src/analysis/normed_space/basic.lean

@@ -94,8 +94,8 @@ lemma norm_zsmul (α) [normed_field α] [normed_space α β] (n : ℤ) (x : β)
   ‖n • x‖ = ‖(n : α)‖ * ‖x‖ :=
 by rw [← norm_smul, ← int.smul_one_eq_coe, smul_assoc, one_smul]
 
-@[simp] lemma abs_norm_eq_norm (z : β) : |‖z‖| = ‖z‖ :=
-  (abs_eq (norm_nonneg z)).mpr (or.inl rfl)
+@[simp] lemma abs_norm (z : β) : |‖z‖| = ‖z‖ :=
+abs_of_nonneg $ norm_nonneg z
 
 lemma inv_norm_smul_mem_closed_unit_ball [normed_space ℝ β] (x : β) :
   ‖x‖⁻¹ • x ∈ closed_ball (0 : β) 1 :=
@@ -225,8 +225,8 @@ noncomputable def homeomorph_unit_ball [normed_space ℝ E] :
 { to_fun := λ x, ⟨(1 + ‖x‖^2).sqrt⁻¹ • x, begin
     have : 0 < 1 + ‖x‖ ^ 2, by positivity,
     rw [mem_ball_zero_iff, norm_smul, real.norm_eq_abs, abs_inv, ← div_eq_inv_mul,
-      div_lt_one (abs_pos.mpr $ real.sqrt_ne_zero'.mpr this), ← abs_norm_eq_norm x, ← sq_lt_sq,
-      abs_norm_eq_norm, real.sq_sqrt this.le],
+      div_lt_one (abs_pos.mpr $ real.sqrt_ne_zero'.mpr this), ← abs_norm x, ← sq_lt_sq,
+      abs_norm, real.sq_sqrt this.le],
     exact lt_one_add _,
   end⟩,
   inv_fun := λ y, (1 - ‖(y : E)‖^2).sqrt⁻¹ • (y : E),

src/analysis/normed_space/lp_space.lean

@@ -961,7 +961,7 @@ begin
   rw ← H at hs,
   have : |‖∑ i in s, lp.single p i (f i : E i) - f‖ ^ p.to_real|
     = ‖∑ i in s, lp.single p i (f i : E i) - f‖ ^ p.to_real,
-  { simp only [real.abs_rpow_of_nonneg (norm_nonneg _), abs_norm_eq_norm] },
+  { simp only [real.abs_rpow_of_nonneg (norm_nonneg _), abs_norm] },
   linarith
 end
 

src/analysis/normed_space/star/continuous_functional_calculus.lean

@@ -146,7 +146,7 @@ begin
   refine ⟨u.unit_of_nearby _ _, rfl⟩,
   simp only [complex.abs_of_real, map_inv₀, units.coe_map, units.coe_inv, ring_hom.coe_monoid_hom,
     ring_hom.to_monoid_hom_eq_coe, units.coe_mk0, units.coe_map_inv, norm_algebra_map',
-    inv_inv, complex.norm_eq_abs, abs_norm_eq_norm, subtype.val_eq_coe, coe_coe],
+    inv_inv, complex.norm_eq_abs, abs_norm, subtype.val_eq_coe, coe_coe],
   /- Since `a` is invertible, by `spectrum_star_mul_self_of_is_star_normal`, the spectrum (in `A`)
   of `star a * a` is contained in the half-open interval `(0, ‖star a * a‖]`. Therefore, by basic
   spectral mapping properties, the spectrum of `‖star a * a‖ • 1 - star a * a` is contained in