feat(data/complex/basic): bundle complex.abs (#16347)

Doing this this way round makes the refactor in #16340 much easier. I will follow up this PR with similar PRs for `padic_norm` and `padic_norm_e`.



Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/algebra/order/absolute_value.lean

@@ -57,6 +57,8 @@ instance subadditive_hom_class : subadditive_hom_class (absolute_value R S) R S
 { map_add_le_add := λ f, f.add_le',
   ..absolute_value.zero_hom_class }
 
+@[simp] lemma coe_mk (f : R →ₙ* S) {h₁ h₂ h₃} : ((absolute_value.mk f h₁ h₂ h₃) : R → S) = f := rfl
+
 /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
 directly. -/
 instance : has_coe_to_fun (absolute_value R S) (λ f, R → S) := fun_like.has_coe_to_fun
@@ -68,6 +70,8 @@ protected theorem nonneg (x : R) : 0 ≤ abv x := abv.nonneg' x
 protected theorem add_le (x y : R) : abv (x + y) ≤ abv x + abv y := abv.add_le' x y
 @[simp] protected theorem map_mul (x y : R) : abv (x * y) = abv x * abv y := abv.map_mul' x y
 
+protected theorem ne_zero_iff {x : R} : abv x ≠ 0 ↔ x ≠ 0 := abv.eq_zero.not
+
 protected theorem pos {x : R} (hx : x ≠ 0) : 0 < abv x :=
 lt_of_le_of_ne (abv.nonneg x) (ne.symm $ mt abv.eq_zero.mp hx)
 

src/analysis/complex/basic.lean

@@ -40,14 +40,14 @@ instance : has_norm ℂ := ⟨abs⟩
 
 instance : normed_add_comm_group ℂ :=
 normed_add_comm_group.of_core ℂ
-{ norm_eq_zero_iff := λ z, abs_eq_zero,
-  triangle := abs_add,
-  norm_neg := abs_neg }
+{ norm_eq_zero_iff := λ x, abs.eq_zero,
+  triangle := abs.add_le,
+  norm_neg := abs.map_neg }
 
 instance : normed_field ℂ :=
 { norm := abs,
   dist_eq := λ _ _, rfl,
-  norm_mul' := abs_mul,
+  norm_mul' := map_mul abs,
   .. complex.field, .. complex.normed_add_comm_group }
 
 instance : densely_normed_field ℂ :=
@@ -57,8 +57,8 @@ instance : densely_normed_field ℂ :=
 
 instance {R : Type*} [normed_field R] [normed_algebra R ℝ] : normed_algebra R ℂ :=
 { norm_smul_le := λ r x, begin
-    rw [norm_eq_abs, norm_eq_abs, ←algebra_map_smul ℝ r x, algebra.smul_def, abs_mul,
-      ←norm_algebra_map' ℝ r, coe_algebra_map, abs_of_real],
+    rw [norm_eq_abs, norm_eq_abs, ←algebra_map_smul ℝ r x, algebra.smul_def, map_mul,
+        ←norm_algebra_map' ℝ r, coe_algebra_map, abs_of_real],
     refl,
   end,
   to_algebra := complex.algebra }

src/analysis/complex/circle.lean

@@ -47,7 +47,7 @@ lemma circle_def : ↑circle = {z : ℂ | abs z = 1} := set.ext $ λ z, mem_circ
 mem_circle_iff_abs.mp z.2
 
 lemma mem_circle_iff_norm_sq {z : ℂ} : z ∈ circle ↔ norm_sq z = 1 :=
-by rw [mem_circle_iff_abs, complex.abs, real.sqrt_eq_one]
+by simp [complex.abs]
 
 @[simp] lemma norm_sq_eq_of_mem_circle (z : circle) : norm_sq z = 1 := by simp [norm_sq_eq_abs]
 
@@ -72,7 +72,7 @@ instance : topological_group circle := metric.sphere.topological_group
 
 /-- If `z` is a nonzero complex number, then `conj z / z` belongs to the unit circle. -/
 @[simps] def circle.of_conj_div_self (z : ℂ) (hz : z ≠ 0) : circle :=
-⟨conj z / z, mem_circle_iff_abs.2 $ by rw [complex.abs_div, abs_conj, div_self (abs_ne_zero.2 hz)]⟩
+⟨conj z / z, mem_circle_iff_abs.2 $ by rw [map_div₀, abs_conj, div_self (complex.abs.ne_zero hz)]⟩
 
 /-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`. -/
 def exp_map_circle : C(ℝ, circle) :=

src/analysis/complex/isometry.lean

@@ -35,7 +35,7 @@ local notation (name := complex.abs) `|` x `|` := complex.abs x
 rotation. -/
 def rotation : circle →* (ℂ ≃ₗᵢ[ℝ] ℂ) :=
 { to_fun := λ a,
-  { norm_map' := λ x, show |a * x| = |x|, by rw [complex.abs_mul, abs_coe_circle, one_mul],
+  { norm_map' := λ x, show |a * x| = |x|, by rw [map_mul, abs_coe_circle, one_mul],
     ..distrib_mul_action.to_linear_equiv ℝ ℂ a },
   map_one' := linear_isometry_equiv.ext $ one_smul _,
   map_mul' := λ _ _, linear_isometry_equiv.ext $ mul_smul _ _ }
@@ -82,7 +82,7 @@ lemma linear_isometry.im_apply_eq_im_or_neg_of_re_apply_eq_re {f : ℂ →ₗᵢ
   (f z).im = z.im ∨ (f z).im = -z.im :=
 begin
   have h₁ := f.norm_map z,
-  simp only [complex.abs, norm_eq_abs] at h₁,
+  simp only [complex.abs_def, norm_eq_abs] at h₁,
   rwa [real.sqrt_inj (norm_sq_nonneg _) (norm_sq_nonneg _), norm_sq_apply (f z), norm_sq_apply z,
     h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁,
 end

src/analysis/complex/phragmen_lindelof.lean

@@ -85,12 +85,12 @@ begin
   have : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ →
     (λ z : ℂ, expR (B₁ * (abs z) ^ c₁)) =O[comap complex.abs at_top ⊓ l]
       (λ z, expR (B₂ * (abs z) ^ c₂)),
-  { have : ∀ᶠ z : ℂ in comap abs at_top ⊓ l, 1 ≤ abs z,
+  { have : ∀ᶠ z : ℂ in comap complex.abs at_top ⊓ l, 1 ≤ abs z,
       from ((eventually_ge_at_top 1).comap _).filter_mono inf_le_left,
     refine λ c₁ c₂ B₁ B₂ hc hB₀ hB, is_O.of_bound 1 (this.mono $ λ z hz, _),
     rw [one_mul, real.norm_eq_abs, real.norm_eq_abs, real.abs_exp, real.abs_exp, real.exp_le_exp],
     exact mul_le_mul hB (real.rpow_le_rpow_of_exponent_le hz hc)
-      (real.rpow_nonneg_of_nonneg (abs_nonneg _) _) hB₀ },
+      (real.rpow_nonneg_of_nonneg (complex.abs.nonneg _) _) hB₀ },
   rcases hBf with ⟨cf, hcf, Bf, hOf⟩, rcases hBg with ⟨cg, hcg, Bg, hOg⟩,
   refine ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), _⟩,
   refine (hOf.trans $ this _ _ _).sub (hOg.trans $ this _ _ _),
@@ -469,7 +469,7 @@ begin
     simpa only [mem_re_prod_im, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using hw.symm },
   refine quadrant_I (hd.comp (differentiable_id.mul_const _).diff_cont_on_cl H)
     (Exists₃.imp (λ c hc B hO, _) hB) him (λ x hx, _) hz_im hz_re,
-  { simpa only [(∘), complex.abs_mul, abs_I, mul_one]
+  { simpa only [(∘), map_mul, abs_I, mul_one]
       using hO.comp_tendsto ((tendsto_mul_right_cobounded I_ne_zero).inf H.tendsto) },
   { rw [comp_app, mul_assoc, I_mul_I, mul_neg_one, ← of_real_neg],
     exact hre _ (neg_nonpos.2 hx) }
@@ -534,7 +534,7 @@ begin
   refine quadrant_I (hd.comp differentiable_neg.diff_cont_on_cl H) _ (λ x hx, _) (λ x hx, _)
     hz_re hz_im,
   { refine Exists₃.imp (λ c hc B hO, _) hB,
-    simpa only [(∘), complex.abs_neg]
+    simpa only [(∘), complex.abs.map_neg]
       using hO.comp_tendsto (tendsto_neg_cobounded.inf H.tendsto) },
   { rw [comp_app, ← of_real_neg],
     exact hre (-x) (neg_nonpos.2 hx) },
@@ -601,7 +601,7 @@ begin
   refine quadrant_II (hd.comp differentiable_neg.diff_cont_on_cl H) _ (λ x hx, _) (λ x hx, _)
     hz_re hz_im,
   { refine Exists₃.imp (λ c hc B hO, _) hB,
-    simpa only [(∘), complex.abs_neg]
+    simpa only [(∘), complex.abs.map_neg]
       using hO.comp_tendsto (tendsto_neg_cobounded.inf H.tendsto) },
   { rw [comp_app, ← of_real_neg],
     exact hre (-x) (neg_nonneg.2 hx) },
@@ -814,7 +814,7 @@ begin
       ... = abs z ^ (1 : ℝ) : (real.rpow_one _).symm
       ... ≤ abs z ^ (max c 1) : real.rpow_le_rpow_of_exponent_le hr (le_max_right _ _) },
     { exact mul_le_mul (le_max_left _ _) (real.rpow_le_rpow_of_exponent_le hr (le_max_left _ _))
-        (real.rpow_nonneg_of_nonneg (abs_nonneg _) _) (le_max_right _ _) } },
+        (real.rpow_nonneg_of_nonneg (complex.abs.nonneg _) _) (le_max_right _ _) } },
   { rw tendsto_zero_iff_norm_tendsto_zero, simp only [hg],
     exact hre n },
   { rw [hg, of_real_mul_re, I_re, mul_zero, real.exp_zero, one_pow, one_mul],
@@ -845,7 +845,7 @@ begin
   suffices : eq_on (f - g) 0 {z : ℂ | 0 ≤ z.re},
     by simpa only [eq_on, pi.sub_apply, pi.zero_apply, sub_eq_zero] using this,
   refine eq_zero_on_right_half_plane_of_superexponential_decay (hfd.sub hgd) _ hre _,
-  { set l : filter ℂ := comap abs at_top ⊓ 𝓟 {z : ℂ | 0 < z.re},
+  { set l : filter ℂ := comap complex.abs at_top ⊓ 𝓟 {z : ℂ | 0 < z.re},
     suffices : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → B₁ ≤ B₂ → 0 ≤ B₂ →
       (λ z, expR (B₁ * abs z ^ c₁)) =O[l] (λ z, expR (B₂ * abs z ^ c₂)),
     { rcases hfexp with ⟨cf, hcf, Bf, hOf⟩, rcases hgexp with ⟨cg, hcg, Bg, hOg⟩,
@@ -857,7 +857,7 @@ begin
     refine is_O.of_bound 1 (this.mono $ λ z hz, _),
     simp only [real.norm_of_nonneg (real.exp_pos _).le, real.exp_le_exp, one_mul],
     exact mul_le_mul hB (real.rpow_le_rpow_of_exponent_le hz hc)
-      (real.rpow_nonneg_of_nonneg (abs_nonneg _) _) hB₂ },
+      (real.rpow_nonneg_of_nonneg (complex.abs.nonneg _) _) hB₂ },
   { rcases hfim with ⟨Cf, hCf⟩, rcases hgim with ⟨Cg, hCg⟩,
     exact ⟨Cf + Cg, λ x, norm_sub_le_of_le (hCf x) (hCg x)⟩ }
 end

src/analysis/complex/polynomial.lean

@@ -15,7 +15,7 @@ This file proves that every nonconstant complex polynomial has a root.
 As a consequence, the complex numbers are algebraically closed.
 -/
 
-open complex polynomial metric filter is_absolute_value set
+open complex polynomial metric filter set
 open_locale classical
 
 namespace complex
@@ -37,10 +37,10 @@ have hg : g * (X - C z₀) ^ n = f - C (f.eval z₀),
   from div_by_monic_mul_pow_root_multiplicity_eq _ _,
 have hn0 : n ≠ 0, from λ hn0, by simpa [g, hn0] using hg0,
 let ⟨δ', hδ'₁, hδ'₂⟩ := continuous_iff.1 (polynomial.continuous g) z₀
-  ((g.eval z₀).abs) (complex.abs_pos.2 hg0) in
+  ((g.eval z₀).abs) (abs.pos hg0) in
 let δ := min (min (δ' / 2) 1) (((f.eval z₀).abs / (g.eval z₀).abs) / 2) in
-have hf0' : 0 < (f.eval z₀).abs, from complex.abs_pos.2 hf0,
-have hg0' : 0 < abs (eval z₀ g), from complex.abs_pos.2 hg0,
+have hf0' : 0 < (f.eval z₀).abs, from abs.pos hf0,
+have hg0' : 0 < (eval z₀ g).abs, from abs.pos hg0,
 have hfg0 : 0 < (f.eval z₀).abs / abs (eval z₀ g), from div_pos hf0' hg0',
 have hδ0 : 0 < δ, from lt_min (lt_min (half_pos hδ'₁) (by norm_num)) (half_pos hfg0),
 have hδ : ∀ z : ℂ, abs (z - z₀) = δ → abs (g.eval z - g.eval z₀) < (g.eval z₀).abs,
@@ -65,31 +65,31 @@ have hF₂ : (F.eval z').abs = (f.eval z₀).abs - (g.eval z₀).abs * δ ^ n,
   from calc (F.eval z').abs = (f.eval z₀ - f.eval z₀ * (g.eval z₀).abs
     * δ ^ n / (f.eval z₀).abs).abs : congr_arg abs hF₁
   ... = abs (f.eval z₀) * complex.abs (1 - (g.eval z₀).abs * δ ^ n /
-      (f.eval z₀).abs : ℝ) : by rw [← complex.abs_mul];
+      (f.eval z₀).abs : ℝ) : by rw [←map_mul];
         exact congr_arg complex.abs
-          (by simp [mul_add, add_mul, mul_assoc, div_eq_mul_inv, sub_eq_add_neg])
+          (by simp only [mul_add, mul_assoc, div_eq_mul_inv, sub_eq_add_neg, of_real_add, mul_one,
+                         of_real_one, of_real_neg, of_real_mul, of_real_pow, of_real_inv, mul_neg])
   ... = _ : by rw [complex.abs_of_nonneg (sub_nonneg.2 (le_of_lt hδs)),
       mul_sub, mul_div_cancel' _ (ne.symm (ne_of_lt hf0')), mul_one],
 have hef0 : abs (eval z₀ g) * (eval z₀ f).abs ≠ 0,
-  from mul_ne_zero (mt complex.abs_eq_zero.1 hg0) (mt complex.abs_eq_zero.1 hf0),
+  from mul_ne_zero (abs.ne_zero hg0) (abs.ne_zero hf0),
 have hz'z₀ : abs (z' - z₀) = δ,
-  by simp [z', mul_assoc, mul_left_comm _ (_ ^ n), mul_comm _ (_ ^ n),
-    mul_comm (eval z₀ f).abs, _root_.mul_div_cancel _ hef0, of_real_mul,
-    neg_mul, neg_div, is_absolute_value.abv_pow complex.abs,
-    complex.abs_of_nonneg hδ0.le, real.pow_nat_rpow_nat_inv hδ0.le hn0],
+  by simp only [z', mul_assoc, mul_left_comm _ (_ ^ n), mul_comm _ (_ ^ n), mul_comm (eval _ f).abs,
+                _root_.mul_div_cancel _ hef0, of_real_mul, neg_mul, neg_div, map_pow, abs_of_real,
+                add_sub_cancel, abs_cpow_inv_nat, absolute_value.map_neg, map_div₀, map_mul,
+                abs_abs, complex.abs_of_nonneg hδ0.le, real.pow_nat_rpow_nat_inv hδ0.le hn0],
 have hF₃ : (f.eval z' - F.eval z').abs < (g.eval z₀).abs * δ ^ n,
   from calc (f.eval z' - F.eval z').abs
       = (g.eval z' - g.eval z₀).abs * (z' - z₀).abs ^ n :
-        by rw [← eq_sub_iff_add_eq.1 hg, ← is_absolute_value.abv_pow complex.abs,
-            ← complex.abs_mul, sub_mul];
-          simp [F, eval_pow, eval_add, eval_mul, eval_sub, eval_C, eval_X, eval_neg, add_sub_cancel,
-                sub_eq_add_neg, add_assoc]
+        by rw [← eq_sub_iff_add_eq.1 hg, ←map_pow abs, ←map_mul, sub_mul];
+           simp only [eval_pow, eval_add, eval_mul, eval_C, eval_X, eval_neg, sub_eq_add_neg,
+                      add_assoc, neg_add_rev, add_neg_cancel_comm_assoc]
   ... = (g.eval z' - g.eval z₀).abs * δ ^ n : by rw hz'z₀
   ... < _ : (mul_lt_mul_right (pow_pos hδ0 _)).2 (hδ _ hz'z₀),
 lt_irrefl (f.eval z₀).abs $
   calc (f.eval z₀).abs ≤ (f.eval z').abs : hz₀ _
     ... = (F.eval z' + (f.eval z' - F.eval z')).abs : by simp
-    ... ≤ (F.eval z').abs + (f.eval z' - F.eval z').abs : complex.abs_add _ _
+    ... ≤ (F.eval z').abs + (f.eval z' - F.eval z').abs : abs.add_le _ _
     ... < (f.eval z₀).abs - (g.eval z₀).abs * δ ^ n + (g.eval z₀).abs * δ ^ n :
       add_lt_add_of_le_of_lt (by rw hF₂) hF₃
     ... = (f.eval z₀).abs : sub_add_cancel _ _

src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean

@@ -63,7 +63,7 @@ bounded_filter_subalgebra at_im_infty
 
 lemma prod_of_bounded_is_bounded {f g : ℍ → ℂ} (hf : is_bounded_at_im_infty f)
   (hg : is_bounded_at_im_infty g) : is_bounded_at_im_infty (f * g) :=
-by simpa only [pi.one_apply, mul_one, norm_eq_abs, complex.abs_mul] using hf.mul hg
+by simpa only [pi.one_apply, mul_one, norm_eq_abs] using hf.mul hg
 
 @[simp] lemma bounded_mem (f : ℍ → ℂ) :
   is_bounded_at_im_infty f ↔ ∃ (M A : ℝ), ∀ z : ℍ, A ≤ im z → abs (f z) ≤ M :=

src/analysis/special_functions/compare_exp.lean

@@ -139,7 +139,7 @@ lemma is_o_cpow_exp (hl : is_exp_cmp_filter l) (a : ℂ) {b : ℝ} (hb : 0 < b)
   (λ z, z ^ a) =o[l] (λ z, exp (b * z)) :=
 calc (λ z, z ^ a) =Θ[l] λ z, abs z ^ re a : is_Theta_cpow_const_rpow $ λ _ _, hl.eventually_ne
 ... =ᶠ[l] λ z, real.exp (re a * real.log (abs z)) : hl.eventually_ne.mono $
-  λ z hz, by simp only [real.rpow_def_of_pos (abs_pos.2 hz), mul_comm]
+  λ z hz, by simp only [real.rpow_def_of_pos, abs.pos hz, mul_comm]
 ... =o[l] λ z, exp (b * z) : is_o.of_norm_right $
   begin
     simp only [norm_eq_abs, abs_exp, of_real_mul_re, real.is_o_exp_comp_exp_comp],

src/analysis/special_functions/complex/arg.lean

@@ -40,9 +40,10 @@ by unfold arg; split_ifs;
 
 lemma cos_arg {x : ℂ} (hx : x ≠ 0) : real.cos (arg x) = x.re / x.abs :=
 begin
-  have habs : 0 < abs x := abs_pos.2 hx,
+  have habs : 0 < abs x := abs.pos hx,
   have him : |im x / abs x| ≤ 1,
-  { rw [_root_.abs_div, abs_abs], exact div_le_one_of_le x.abs_im_le_abs x.abs_nonneg },
+  { rw [_root_.abs_div, abs_abs],
+    exact div_le_one_of_le x.abs_im_le_abs (abs.nonneg x) },
   rw abs_le at him,
   rw arg, split_ifs with h₁ h₂ h₂,
   { rw [real.cos_arcsin]; field_simp [real.sqrt_sq, habs.le, *] },
@@ -62,7 +63,7 @@ end
 begin
   rcases eq_or_ne x 0 with (rfl|hx),
   { simp },
-  { have : abs x ≠ 0 := abs_ne_zero.2 hx,
+  { have : abs x ≠ 0 := abs.ne_zero hx,
     ext; field_simp [sin_arg, cos_arg hx, this, mul_comm (abs x)] }
 end
 
@@ -85,8 +86,7 @@ by { ext x, simp only [mem_sphere_zero_iff_norm, norm_eq_abs, abs_eq_one_iff, me
 lemma arg_mul_cos_add_sin_mul_I {r : ℝ} (hr : 0 < r) {θ : ℝ} (hθ : θ ∈ Ioc (-π) π) :
   arg (r * (cos θ + sin θ * I)) = θ :=
 begin
-  have hπ := real.pi_pos,
-  simp only [arg, abs_mul, abs_cos_add_sin_mul_I, abs_of_nonneg hr.le, mul_one],
+  simp only [arg, map_mul, abs_cos_add_sin_mul_I, abs_of_nonneg hr.le, mul_one],
   simp only [of_real_mul_re, of_real_mul_im, neg_im, ← of_real_cos, ← of_real_sin,
     ← mk_eq_add_mul_I, neg_div, mul_div_cancel_left _ hr.ne',
     mul_nonneg_iff_right_nonneg_of_pos hr],
@@ -127,7 +127,7 @@ begin
   rw [← abs_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N,
     ← sin_add_int_mul_two_pi _ N],
   simp only [← of_real_one, ← of_real_bit0, ← of_real_mul, ← of_real_add, ← of_real_int_cast],
-  rwa [arg_mul_cos_add_sin_mul_I (abs_pos.2 hz) hN]
+  rwa [arg_mul_cos_add_sin_mul_I (abs.pos hz) hN]
 end
 
 @[simp] lemma range_arg : range arg = Ioc (-π) π :=
@@ -147,7 +147,7 @@ begin
   calc 0 ≤ arg z ↔ 0 ≤ real.sin (arg z) :
     ⟨λ h, real.sin_nonneg_of_mem_Icc ⟨h, arg_le_pi z⟩,
       by { contrapose!, intro h, exact real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _) }⟩
-  ... ↔ _ : by rw [sin_arg, le_div_iff (abs_pos.2 h₀), zero_mul]
+  ... ↔ _ : by rw [sin_arg, le_div_iff (abs.pos h₀), zero_mul]
 end
 
 @[simp] lemma arg_neg_iff {z : ℂ} : arg z < 0 ↔ z.im < 0 :=
@@ -157,16 +157,16 @@ lemma arg_real_mul (x : ℂ) {r : ℝ} (hr : 0 < r) : arg (r * x) = arg x :=
 begin
   rcases eq_or_ne x 0 with (rfl|hx), { rw mul_zero },
   conv_lhs { rw [← abs_mul_cos_add_sin_mul_I x, ← mul_assoc, ← of_real_mul,
-    arg_mul_cos_add_sin_mul_I (mul_pos hr (abs_pos.2 hx)) x.arg_mem_Ioc] }
+    arg_mul_cos_add_sin_mul_I (mul_pos hr (abs.pos hx)) x.arg_mem_Ioc] }
 end
 
 lemma arg_eq_arg_iff {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
   arg x = arg y ↔ (abs y / abs x : ℂ) * x = y :=
 begin
-  simp only [ext_abs_arg_iff, abs_mul, abs_div, abs_of_real, abs_abs,
-    div_mul_cancel _ (abs_ne_zero.2 hx), eq_self_iff_true, true_and],
+  simp only [ext_abs_arg_iff, map_mul, map_div₀, abs_of_real, abs_abs,
+    div_mul_cancel _ (abs.ne_zero hx), eq_self_iff_true, true_and],
   rw [← of_real_div, arg_real_mul],
-  exact div_pos (abs_pos.2 hy) (abs_pos.2 hx)
+  exact div_pos (abs.pos hy) (abs.pos hx)
 end
 
 @[simp] lemma arg_one : arg 1 = 0 :=
@@ -186,7 +186,7 @@ begin
   by_cases h : x = 0,
   { simp only [h, zero_div, complex.zero_im, complex.arg_zero, real.tan_zero, complex.zero_re] },
   rw [real.tan_eq_sin_div_cos, sin_arg, cos_arg h,
-      div_div_div_cancel_right _ (abs_ne_zero.2 h)]
+      div_div_div_cancel_right _ (abs.ne_zero h)]
 end
 
 lemma arg_of_real_of_nonneg {x : ℝ} (hx : 0 ≤ x) : arg x = 0 :=
@@ -196,7 +196,7 @@ lemma arg_eq_zero_iff {z : ℂ} : arg z = 0 ↔ 0 ≤ z.re ∧ z.im = 0 :=
 begin
   refine ⟨λ h, _, _⟩,
   { rw [←abs_mul_cos_add_sin_mul_I z, h],
-    simp [abs_nonneg] },
+    simp [abs.nonneg] },
   { cases z with x y,
     rintro ⟨h, rfl : y = 0⟩,
     exact arg_of_real_of_nonneg h }
@@ -296,7 +296,7 @@ begin
     rw [iff_false, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub,
       real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ←
       _root_.abs_of_nonneg him, abs_im_lt_abs],
-    exacts [hre.ne, abs_pos.2 $ ne_of_apply_ne re hre.ne] },
+    exacts [hre.ne, abs.pos $ ne_of_apply_ne re hre.ne] },
   { simp only [him],
     rw [iff_true, arg_of_re_neg_of_im_neg hre him],
     exact (sub_le_self _ real.pi_pos.le).trans (real.arcsin_le_pi_div_two _) }
@@ -314,7 +314,7 @@ begin
   { simp only [him.not_le],
     rw [iff_false, not_le, arg_of_re_neg_of_im_neg hre him, sub_lt_iff_lt_add', ← sub_eq_add_neg,
       sub_half, real.arcsin_lt_pi_div_two, div_lt_one, neg_im, ← abs_of_neg him, abs_im_lt_abs],
-    exacts [hre.ne, abs_pos.2 $ ne_of_apply_ne re hre.ne] }
+    exacts [hre.ne, abs.pos $ ne_of_apply_ne re hre.ne] }
 end
 
 @[simp] lemma abs_arg_le_pi_div_two_iff {z : ℂ} : |arg z| ≤ π / 2 ↔ 0 ≤ re z :=
@@ -434,7 +434,7 @@ by rw [←one_mul (_ + _), ←of_real_one, arg_mul_cos_add_sin_mul_I_coe_angle z
 lemma arg_mul_coe_angle {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
   (arg (x * y) : real.angle) = arg x + arg y :=
 begin
-  convert arg_mul_cos_add_sin_mul_I_coe_angle (mul_pos (abs_pos.2 hx) (abs_pos.2 hy))
+  convert arg_mul_cos_add_sin_mul_I_coe_angle (mul_pos (abs.pos hx) (abs.pos hy))
                                               (arg x + arg y : real.angle) using 3,
   simp_rw [←real.angle.coe_add, real.angle.sin_coe, real.angle.cos_coe, of_real_cos,
            of_real_sin, cos_add_sin_I, of_real_add, add_mul, exp_add, of_real_mul],
@@ -496,7 +496,7 @@ lemma arg_eq_nhds_of_im_neg (hz : im z < 0) :
 
 lemma continuous_at_arg (h : 0 < x.re ∨ x.im ≠ 0) : continuous_at arg x :=
 begin
-  have h₀ : abs x ≠ 0, { rw abs_ne_zero, rintro rfl, simpa using h },
+  have h₀ : abs x ≠ 0, { rw abs.ne_zero_iff, rintro rfl, simpa using h },
   rw [← lt_or_lt_iff_ne] at h,
   rcases h with (hx_re|hx_im|hx_im),
   exacts [(real.continuous_at_arcsin.comp (continuous_im.continuous_at.div