diff --git a/src/algebra/order/absolute_value.lean b/src/algebra/order/absolute_value.lean
index e5036eb1c1d9c..3bfce7120fe8a 100644
--- a/src/algebra/order/absolute_value.lean
+++ b/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)
 
diff --git a/src/analysis/complex/basic.lean b/src/analysis/complex/basic.lean
index 13ccea2e8b15c..1e787adf61a56 100644
--- a/src/analysis/complex/basic.lean
+++ b/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 }
diff --git a/src/analysis/complex/circle.lean b/src/analysis/complex/circle.lean
index c34547179b959..1b331d9c74203 100644
--- a/src/analysis/complex/circle.lean
+++ b/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) :=
diff --git a/src/analysis/complex/isometry.lean b/src/analysis/complex/isometry.lean
index 88de13fee8aa5..47ab817740365 100644
--- a/src/analysis/complex/isometry.lean
+++ b/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
diff --git a/src/analysis/complex/phragmen_lindelof.lean b/src/analysis/complex/phragmen_lindelof.lean
index afcff7594f579..d08247ab107d1 100644
--- a/src/analysis/complex/phragmen_lindelof.lean
+++ b/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
diff --git a/src/analysis/complex/polynomial.lean b/src/analysis/complex/polynomial.lean
index 5065f84e1f585..af6f3afcafdbd 100644
--- a/src/analysis/complex/polynomial.lean
+++ b/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 _ _
diff --git a/src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean b/src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean
index d8732563824f1..a56a5361b5f25 100644
--- a/src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean
+++ b/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 :=
diff --git a/src/analysis/special_functions/compare_exp.lean b/src/analysis/special_functions/compare_exp.lean
index 9f7ec46b1b750..653f01558aa33 100644
--- a/src/analysis/special_functions/compare_exp.lean
+++ b/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],
diff --git a/src/analysis/special_functions/complex/arg.lean b/src/analysis/special_functions/complex/arg.lean
index 911713e79f06a..847a93fcd6814 100644
--- a/src/analysis/special_functions/complex/arg.lean
+++ b/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
diff --git a/src/analysis/special_functions/complex/log.lean b/src/analysis/special_functions/complex/log.lean
index 8d583cf814b00..24ee1eb4a85b5 100644
--- a/src/analysis/special_functions/complex/log.lean
+++ b/src/analysis/special_functions/complex/log.lean
@@ -33,9 +33,9 @@ lemma log_im_le_pi (x : ℂ) : (log x).im ≤ π := by simp only [log_im, arg_le
 
 lemma exp_log {x : ℂ} (hx : x ≠ 0) : exp (log x) = x :=
 by rw [log, exp_add_mul_I, ← of_real_sin, sin_arg, ← of_real_cos, cos_arg hx,
-  ← of_real_exp, real.exp_log (abs_pos.2 hx), mul_add, of_real_div, of_real_div,
-  mul_div_cancel' _ (of_real_ne_zero.2 (mt abs_eq_zero.1 hx)), ← mul_assoc,
-  mul_div_cancel' _ (of_real_ne_zero.2 (mt abs_eq_zero.1 hx)), re_add_im]
+  ← of_real_exp, real.exp_log (abs.pos hx), mul_add, of_real_div, of_real_div,
+  mul_div_cancel' _ (of_real_ne_zero.2 $ abs.ne_zero hx), ← mul_assoc,
+  mul_div_cancel' _ (of_real_ne_zero.2 $ abs.ne_zero hx), re_add_im]
 
 @[simp] lemma range_exp : range exp = {0}ᶜ :=
 set.ext $ λ x, ⟨by { rintro ⟨x, rfl⟩, exact exp_ne_zero x }, λ hx, ⟨log x, exp_log hx⟩⟩
@@ -157,7 +157,7 @@ begin
   refine continuous_at.add _ _,
   { refine continuous_of_real.continuous_at.comp _,
     refine (real.continuous_at_log _).comp complex.continuous_abs.continuous_at,
-    rw abs_ne_zero,
+    rw complex.abs.ne_zero_iff,
     rintro rfl,
     simpa using h },
   { have h_cont_mul : continuous (λ x : ℂ, x * I), from continuous_id'.mul continuous_const,
diff --git a/src/analysis/special_functions/gamma.lean b/src/analysis/special_functions/gamma.lean
index da22edf4b5bb9..a8e3acda7e0f8 100644
--- a/src/analysis/special_functions/gamma.lean
+++ b/src/analysis/special_functions/gamma.lean
@@ -102,7 +102,7 @@ begin
     refine has_finite_integral.congr (real.Gamma_integral_convergent hs).2 _,
     refine (ae_restrict_iff' measurable_set_Ioi).mpr (ae_of_all _ (λ x hx, _)),
     dsimp only,
-    rw [norm_eq_abs, abs_mul, abs_of_nonneg $ le_of_lt $ exp_pos $ -x,
+    rw [norm_eq_abs, map_mul, abs_of_nonneg $ le_of_lt $ exp_pos $ -x,
       abs_cpow_eq_rpow_re_of_pos hx _],
     simp }
 end
@@ -175,7 +175,7 @@ begin
     refine (_ : continuous_at (λ x:ℂ, x ^ (s - 1)) _).comp continuous_of_real.continuous_at,
     apply continuous_at_cpow_const, rw of_real_re, exact or.inl hx.1, },
   rw ←has_finite_integral_norm_iff,
-  simp_rw [norm_eq_abs, complex.abs_mul],
+  simp_rw [norm_eq_abs, map_mul],
   refine (((real.Gamma_integral_convergent hs).mono_set
     Ioc_subset_Ioi_self).has_finite_integral.congr _).const_mul _,
   rw [eventually_eq, ae_restrict_iff'],
@@ -244,7 +244,7 @@ begin
   have : (λ (e : ℝ), ∥-(e:ℂ) ^ s * (-e).exp∥ ) =ᶠ[at_top] (λ (e : ℝ), e ^ s.re * (-1 * e).exp ),
   { refine eventually_eq_of_mem (Ioi_mem_at_top 0) _,
     intros x hx, dsimp only,
-    rw [norm_eq_abs, abs_mul, abs_neg, abs_cpow_eq_rpow_re_of_pos hx,
+    rw [norm_eq_abs, map_mul, abs.map_neg, abs_cpow_eq_rpow_re_of_pos hx,
       abs_of_nonneg (exp_pos(-x)).le, neg_mul, one_mul],},
   exact (tendsto_congr' this).mpr (tendsto_rpow_mul_exp_neg_mul_at_top_nhds_0 _ _ zero_lt_one),
 end
@@ -411,7 +411,7 @@ begin
   rcases le_or_lt 1 x with h|h,
   { -- case 1 ≤ x
     refine le_add_of_nonneg_of_le (abs_nonneg _) _,
-    rw [dGamma_integrand, dGamma_integrand_real, complex.norm_eq_abs, complex.abs_mul, abs_mul,
+    rw [dGamma_integrand, dGamma_integrand_real, complex.norm_eq_abs, map_mul, abs_mul,
       ←complex.of_real_mul, complex.abs_of_real],
     refine mul_le_mul_of_nonneg_left _ (abs_nonneg _),
     rw complex.abs_cpow_eq_rpow_re_of_pos hx,
@@ -419,7 +419,7 @@ begin
     apply rpow_le_rpow_of_exponent_le h,
     rw [complex.sub_re, complex.one_re], linarith, },
   { refine le_add_of_le_of_nonneg _ (abs_nonneg _),
-    rw [dGamma_integrand, dGamma_integrand_real, complex.norm_eq_abs, complex.abs_mul, abs_mul,
+    rw [dGamma_integrand, dGamma_integrand_real, complex.norm_eq_abs, map_mul, abs_mul,
       ←complex.of_real_mul, complex.abs_of_real],
     refine mul_le_mul_of_nonneg_left _ (abs_nonneg _),
     rw complex.abs_cpow_eq_rpow_re_of_pos hx,
diff --git a/src/analysis/special_functions/polar_coord.lean b/src/analysis/special_functions/polar_coord.lean
index f2679d0c748f5..8b76bf9a13ab3 100644
--- a/src/analysis/special_functions/polar_coord.lean
+++ b/src/analysis/special_functions/polar_coord.lean
@@ -69,7 +69,7 @@ It is a homeomorphism between `ℝ^2 - (-∞, 0]` and `(0, +∞) × (-π, π)`.
   begin
     rintros ⟨x, y⟩ hxy,
     have A : sqrt (x ^ 2 + y ^ 2) = complex.abs (x + y * complex.I),
-      by simp only [complex.abs, complex.norm_sq, pow_two, monoid_with_zero_hom.coe_mk,
+      by simp only [complex.abs_def, complex.norm_sq, pow_two, monoid_with_zero_hom.coe_mk,
         complex.add_re, complex.of_real_re, complex.mul_re, complex.I_re, mul_zero,
         complex.of_real_im, complex.I_im, sub_self, add_zero, complex.add_im,
         complex.mul_im, mul_one, zero_add],
diff --git a/src/analysis/special_functions/pow.lean b/src/analysis/special_functions/pow.lean
index 2302dbe222696..e9d02a03a042f 100644
--- a/src/analysis/special_functions/pow.lean
+++ b/src/analysis/special_functions/pow.lean
@@ -404,32 +404,31 @@ begin
   { rcases eq_or_ne y 0 with rfl|hy; simp * },
   have hne : (x : ℂ) ≠ 0, from of_real_ne_zero.mpr hlt.ne,
   rw [cpow_def_of_ne_zero hne, cpow_def_of_ne_zero (neg_ne_zero.2 hne), ← exp_add, ← add_mul,
-    log, log, abs_neg, arg_of_real_of_neg hlt, ← of_real_neg,
-    arg_of_real_of_nonneg (neg_nonneg.2 hx), of_real_zero, zero_mul, add_zero]
+      log, log, abs.map_neg, arg_of_real_of_neg hlt, ← of_real_neg,
+      arg_of_real_of_nonneg (neg_nonneg.2 hx), of_real_zero, zero_mul, add_zero]
 end
 
 lemma abs_cpow_of_ne_zero {z : ℂ} (hz : z ≠ 0) (w : ℂ) :
   abs (z ^ w) = abs z ^ w.re / real.exp (arg z * im w) :=
 by rw [cpow_def_of_ne_zero hz, abs_exp, mul_re, log_re, log_im, real.exp_sub,
-  real.rpow_def_of_pos (abs_pos.2 hz)]
+  real.rpow_def_of_pos (abs.pos hz)]
 
 lemma abs_cpow_of_imp {z w : ℂ} (h : z = 0 → w.re = 0 → w = 0) :
   abs (z ^ w) = abs z ^ w.re / real.exp (arg z * im w) :=
 begin
-  rcases ne_or_eq z 0 with hz|rfl; [exact (abs_cpow_of_ne_zero hz w), rw abs_zero],
+  rcases ne_or_eq z 0 with hz|rfl; [exact (abs_cpow_of_ne_zero hz w), rw map_zero],
   cases eq_or_ne w.re 0 with hw hw,
   { simp [hw, h rfl hw] },
-  { rw [real.zero_rpow hw, zero_div, zero_cpow, abs_zero],
+  { rw [real.zero_rpow hw, zero_div, zero_cpow, map_zero],
     exact ne_of_apply_ne re hw }
 end
 
 lemma abs_cpow_le (z w : ℂ) : abs (z ^ w) ≤ abs z ^ w.re / real.exp (arg z * im w) :=
 begin
-  by_cases h : z = 0 → w.re = 0 → w = 0,
-  { exact (abs_cpow_of_imp h).le },
-  { push_neg at h,
-    rw [h.1, zero_cpow h.2.2, abs_zero],
-    exact div_nonneg (real.rpow_nonneg_of_nonneg le_rfl _) (real.exp_pos _).le },
+  rcases ne_or_eq z 0 with hz|rfl; [exact (abs_cpow_of_ne_zero hz w).le, rw map_zero],
+  rcases eq_or_ne w 0 with rfl|hw, { simp },
+  rw [zero_cpow hw, map_zero],
+  exact div_nonneg (real.rpow_nonneg_of_nonneg le_rfl _) (real.exp_pos _).le
 end
 
 section
@@ -445,8 +444,8 @@ begin
   refine real.is_Theta_exp_comp_one.2 ⟨π * b, _⟩,
   rw eventually_map at hb ⊢,
   refine hb.mono (λ x hx, _),
-  rw [_root_.abs_mul],
-  exact mul_le_mul (abs_arg_le_pi _) hx (_root_.abs_nonneg _) real.pi_pos.le
+  erw [abs_mul],
+  exact mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) real.pi_pos.le
 end
 
 lemma is_O_cpow_rpow (hl : is_bounded_under (≤) l (λ x, |(g x).im|)) :
@@ -488,7 +487,7 @@ lemma abs_cpow_eq_rpow_re_of_nonneg {x : ℝ} (hx : 0 ≤ x) {y : ℂ} (hy : re
   abs (x ^ y) = x ^ re y :=
 begin
   rcases hx.eq_or_lt with rfl|hlt,
-  { rw [of_real_zero, zero_cpow, abs_zero, real.zero_rpow hy],
+  { rw [of_real_zero, zero_cpow, map_zero, real.zero_rpow hy],
     exact ne_of_apply_ne re hy },
   { exact abs_cpow_eq_rpow_re_of_pos hlt y }
 end
diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean
index b8c91c4bbf0d0..d648b26bb43f3 100644
--- a/src/data/complex/basic.lean
+++ b/src/data/complex/basic.lean
@@ -461,10 +461,56 @@ by simp only [sub_conj, of_real_mul, of_real_one, of_real_bit0, mul_right_comm,
 
 /-! ### Absolute value -/
 
+namespace abs_theory
+-- We develop enough theory to bundle `abs` into an `absolute_value` before making things public;
+-- this is so there's not two versions of it hanging around.
+
+local notation (name := abs) `abs` z := ((norm_sq z).sqrt)
+
+private lemma mul_self_abs (z : ℂ) : (abs z) * (abs z) = norm_sq z :=
+real.mul_self_sqrt (norm_sq_nonneg _)
+
+private lemma abs_nonneg' (z : ℂ) : 0 ≤ abs z :=
+real.sqrt_nonneg _
+
+lemma abs_conj (z : ℂ) : (abs (conj z)) = abs z :=
+by simp
+
+private lemma abs_re_le_abs (z : ℂ) : |z.re| ≤ abs z :=
+begin
+  rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (abs_nonneg' _),
+       abs_mul_abs_self, mul_self_abs],
+  apply re_sq_le_norm_sq
+end
+
+private lemma re_le_abs (z : ℂ) : z.re ≤ abs z :=
+(abs_le.1 (abs_re_le_abs _)).2
+
+private lemma abs_mul (z w : ℂ) : (abs (z * w)) = (abs z) * abs w :=
+by rw [norm_sq_mul, real.sqrt_mul (norm_sq_nonneg _)]
+
+private lemma abs_add (z w : ℂ) : (abs (z + w)) ≤ (abs z) + abs w :=
+(mul_self_le_mul_self_iff (abs_nonneg' (z + w))
+  (add_nonneg (abs_nonneg' z) (abs_nonneg' w))).2 $
+begin
+  rw [mul_self_abs, add_mul_self_eq, mul_self_abs, mul_self_abs, add_right_comm, norm_sq_add,
+      add_le_add_iff_left, mul_assoc, mul_le_mul_left (@zero_lt_two ℝ _ _),
+      ←real.sqrt_mul $ norm_sq_nonneg z, ←norm_sq_conj w, ←map_mul],
+  exact re_le_abs (z * conj w)
+end
+
 /-- The complex absolute value function, defined as the square root of the norm squared. -/
-@[pp_nodot] noncomputable def abs (z : ℂ) : ℝ := (norm_sq z).sqrt
+noncomputable def _root_.complex.abs : absolute_value ℂ ℝ :=
+{ to_fun := λ x, abs x,
+  map_mul' := abs_mul,
+  nonneg' := abs_nonneg',
+  eq_zero' := λ _, (real.sqrt_eq_zero $ norm_sq_nonneg _).trans norm_sq_eq_zero,
+  add_le' := abs_add }
 
-local notation `abs'` := has_abs.abs
+end abs_theory
+
+lemma abs_def : (abs : ℂ → ℝ) = λ z, (norm_sq z).sqrt := rfl
+lemma abs_apply {z : ℂ} : abs z = (norm_sq z).sqrt := rfl
 
 @[simp, norm_cast] lemma abs_of_real (r : ℝ) : abs r = |r| :=
 by simp [abs, norm_sq_of_real, real.sqrt_mul_self_eq_abs]
@@ -488,56 +534,36 @@ by rw [sq_abs, norm_sq_apply, ← sq, ← sq, add_sub_cancel']
 @[simp] lemma sq_abs_sub_sq_im (z : ℂ) : abs z ^ 2 - z.im ^ 2 = z.re ^ 2 :=
 by rw [← sq_abs_sub_sq_re, sub_sub_cancel]
 
-@[simp] lemma abs_zero : abs 0 = 0 := by simp [abs]
-@[simp] lemma abs_one : abs 1 = 1 := by simp [abs]
 @[simp] lemma abs_I : abs I = 1 := by simp [abs]
 
 @[simp] lemma abs_two : abs 2 = 2 :=
 calc abs 2 = abs (2 : ℝ) : by rw [of_real_bit0, of_real_one]
 ... = (2 : ℝ) : abs_of_nonneg (by norm_num)
 
-lemma abs_nonneg (z : ℂ) : 0 ≤ abs z :=
-real.sqrt_nonneg _
-
 @[simp] lemma range_abs : range abs = Ici 0 :=
-subset.antisymm (range_subset_iff.2 abs_nonneg) $ λ x hx, ⟨x, abs_of_nonneg hx⟩
-
-@[simp] lemma abs_eq_zero {z : ℂ} : abs z = 0 ↔ z = 0 :=
-(real.sqrt_eq_zero $ norm_sq_nonneg _).trans norm_sq_eq_zero
-
-lemma abs_ne_zero {z : ℂ} : abs z ≠ 0 ↔ z ≠ 0 :=
-not_congr abs_eq_zero
-
-@[simp] lemma abs_conj (z : ℂ) : abs (conj z) = abs z :=
-by simp [abs]
-
-@[simp] lemma abs_mul (z w : ℂ) : abs (z * w) = abs z * abs w :=
-by rw [abs, norm_sq_mul, real.sqrt_mul (norm_sq_nonneg _)]; refl
+subset.antisymm (range_subset_iff.2 abs.nonneg) $ λ x hx, ⟨x, abs_of_nonneg hx⟩
 
-/-- `complex.abs` as a `monoid_with_zero_hom`. -/
-@[simps] noncomputable def abs_hom : ℂ →*₀ ℝ :=
-{ to_fun := abs,
-  map_zero' := abs_zero,
-  map_one' := abs_one,
-  map_mul' := abs_mul }
+@[simp] lemma abs_conj (z : ℂ) : abs (conj z) = abs z := abs_theory.abs_conj z
 
 @[simp] lemma abs_prod {ι : Type*} (s : finset ι) (f : ι → ℂ) :
   abs (s.prod f) = s.prod (λ i, abs (f i)) :=
-map_prod abs_hom _ _
+map_prod abs _ _
 
 @[simp] lemma abs_pow (z : ℂ) (n : ℕ) : abs (z ^ n) = abs z ^ n :=
-map_pow abs_hom z n
+map_pow abs z n
 
 @[simp] lemma abs_zpow (z : ℂ) (n : ℤ) : abs (z ^ n) = abs z ^ n :=
-map_zpow₀ abs_hom z n
+map_zpow₀ abs z n
 
 lemma abs_re_le_abs (z : ℂ) : |z.re| ≤ abs z :=
-by rw [mul_self_le_mul_self_iff (_root_.abs_nonneg z.re) (abs_nonneg _),
-       abs_mul_abs_self, mul_self_abs];
-   apply re_sq_le_norm_sq
+begin
+  rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (abs.nonneg _),
+       abs_mul_abs_self, mul_self_abs],
+  apply re_sq_le_norm_sq
+end
 
 lemma abs_im_le_abs (z : ℂ) : |z.im| ≤ abs z :=
-by rw [mul_self_le_mul_self_iff (_root_.abs_nonneg z.im) (abs_nonneg _),
+by rw [mul_self_le_mul_self_iff (abs_nonneg z.im) (abs.nonneg _),
        abs_mul_abs_self, mul_self_abs];
    apply im_sq_le_norm_sq
 
@@ -548,67 +574,39 @@ lemma im_le_abs (z : ℂ) : z.im ≤ abs z :=
 (abs_le.1 (abs_im_le_abs _)).2
 
 @[simp] lemma abs_re_lt_abs {z : ℂ} : |z.re| < abs z ↔ z.im ≠ 0 :=
-by rw [abs, real.lt_sqrt (_root_.abs_nonneg _), norm_sq_apply, _root_.sq_abs, ← sq,
-  lt_add_iff_pos_right, mul_self_pos]
+by rw [abs, absolute_value.coe_mk, mul_hom.coe_mk, real.lt_sqrt (abs_nonneg _), norm_sq_apply,
+       _root_.sq_abs, ← sq, lt_add_iff_pos_right, mul_self_pos]
 
 @[simp] lemma abs_im_lt_abs {z : ℂ} : |z.im| < abs z ↔ z.re ≠ 0 :=
 by simpa using @abs_re_lt_abs (z * I)
 
-/--
-The **triangle inequality** for complex numbers.
--/
-lemma abs_add (z w : ℂ) : abs (z + w) ≤ abs z + abs w :=
-(mul_self_le_mul_self_iff (abs_nonneg _)
-  (add_nonneg (abs_nonneg _) (abs_nonneg _))).2 $
-begin
-  rw [mul_self_abs, add_mul_self_eq, mul_self_abs, mul_self_abs,
-      add_right_comm, norm_sq_add, add_le_add_iff_left,
-      mul_assoc, mul_le_mul_left (@zero_lt_two ℝ _ _)],
-  simpa [-mul_re] using re_le_abs (z * conj w)
-end
-
-instance : is_absolute_value abs :=
-{ abv_nonneg  := abs_nonneg,
-  abv_eq_zero := λ _, abs_eq_zero,
-  abv_add     := abs_add,
-  abv_mul     := abs_mul }
-open is_absolute_value
-
 @[simp] lemma abs_abs (z : ℂ) : |(abs z)| = abs z :=
-_root_.abs_of_nonneg (abs_nonneg _)
-
-@[simp] lemma abs_pos {z : ℂ} : 0 < abs z ↔ z ≠ 0 := abv_pos abs
-@[simp] lemma abs_neg : ∀ z, abs (-z) = abs z := abv_neg abs
-lemma abs_sub_comm : ∀ z w, abs (z - w) = abs (w - z) := abv_sub abs
-lemma abs_sub_le : ∀ a b c, abs (a - c) ≤ abs (a - b) + abs (b - c) := abv_sub_le abs
-@[simp] theorem abs_inv : ∀ z, abs z⁻¹ = (abs z)⁻¹ := abv_inv abs
-@[simp] theorem abs_div : ∀ z w, abs (z / w) = abs z / abs w := abv_div abs
-
-lemma abs_abs_sub_le_abs_sub : ∀ z w, |abs z - abs w| ≤ abs (z - w) :=
-abs_abv_sub_le_abv_sub abs
+_root_.abs_of_nonneg (abs.nonneg _)
 
 lemma abs_le_abs_re_add_abs_im (z : ℂ) : abs z ≤ |z.re| + |z.im| :=
-by simpa [re_add_im] using abs_add z.re (z.im * I)
+by simpa [re_add_im] using abs.add_le z.re (z.im * I)
 
 lemma abs_le_sqrt_two_mul_max (z : ℂ) : abs z ≤ real.sqrt 2 * max (|z.re|) (|z.im|) :=
 begin
   cases z with x y,
   simp only [abs, norm_sq_mk, ← sq],
   wlog hle : |x| ≤ |y| := le_total (|x|) (|y|) using [x y, y x] tactic.skip,
-  { calc real.sqrt (x ^ 2 + y ^ 2) ≤ real.sqrt (y ^ 2 + y ^ 2) :
+  { simp only [absolute_value.coe_mk, mul_hom.coe_mk, norm_sq_mk, ←sq],
+    calc real.sqrt (x ^ 2 + y ^ 2) ≤ real.sqrt (y ^ 2 + y ^ 2) :
       real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle) _)
     ... = real.sqrt 2 * max (|x|) (|y|) :
       by rw [max_eq_right hle, ← two_mul, real.sqrt_mul two_pos.le, real.sqrt_sq_eq_abs] },
-  { rwa [add_comm, max_comm] }
+  { dsimp,
+    rwa [add_comm, max_comm] }
 end
 
 lemma abs_re_div_abs_le_one (z : ℂ) : |z.re / z.abs| ≤ 1 :=
 if hz : z = 0 then by simp [hz, zero_le_one]
-else by { simp_rw [_root_.abs_div, abs_abs, div_le_iff (abs_pos.2 hz), one_mul, abs_re_le_abs] }
+else by { simp_rw [_root_.abs_div, abs_abs, div_le_iff (abs.pos hz), one_mul, abs_re_le_abs] }
 
 lemma abs_im_div_abs_le_one (z : ℂ) : |z.im / z.abs| ≤ 1 :=
 if hz : z = 0 then by simp [hz, zero_le_one]
-else by { simp_rw [_root_.abs_div, abs_abs, div_le_iff (abs_pos.2 hz), one_mul, abs_im_le_abs] }
+else by { simp_rw [_root_.abs_div, abs_abs, div_le_iff (abs.pos hz), one_mul, abs_im_le_abs] }
 
 @[simp, norm_cast] lemma abs_cast_nat (n : ℕ) : abs (n : ℂ) = n :=
 by rw [← of_real_nat_cast, abs_of_nonneg (nat.cast_nonneg n)]
@@ -617,7 +615,7 @@ by rw [← of_real_nat_cast, abs_of_nonneg (nat.cast_nonneg n)]
 by rw [← of_real_int_cast, abs_of_real, int.cast_abs]
 
 lemma norm_sq_eq_abs (x : ℂ) : norm_sq x = abs x ^ 2 :=
-by rw [abs, sq, real.mul_self_sqrt (norm_sq_nonneg _)]
+by simp [abs, sq, real.mul_self_sqrt (norm_sq_nonneg _)]
 
 /--
 We put a partial order on ℂ so that `z ≤ w` exactly if `w - z` is real and nonnegative.
@@ -691,6 +689,8 @@ end complex_order
 
 /-! ### Cauchy sequences -/
 
+local notation `abs'` := has_abs.abs
+
 theorem is_cau_seq_re (f : cau_seq ℂ abs) : is_cau_seq abs' (λ n, (f n).re) :=
 λ ε ε0, (f.cauchy ε0).imp $ λ i H j ij,
 lt_of_le_of_lt (by simpa using abs_re_le_abs (f j - f i)) (H _ ij)
@@ -710,7 +710,7 @@ noncomputable def cau_seq_im (f : cau_seq ℂ abs) : cau_seq ℝ abs' :=
 lemma is_cau_seq_abs {f : ℕ → ℂ} (hf : is_cau_seq abs f) :
   is_cau_seq abs' (abs ∘ f) :=
 λ ε ε0, let ⟨i, hi⟩ := hf ε ε0 in
-⟨i, λ j hj, lt_of_le_of_lt (abs_abs_sub_le_abs_sub _ _) (hi j hj)⟩
+⟨i, λ j hj, lt_of_le_of_lt (abs.abs_abv_sub_le_abv_sub _ _) (hi j hj)⟩
 
 /-- The limit of a Cauchy sequence of complex numbers. -/
 noncomputable def lim_aux (f : cau_seq ℂ abs) : ℂ :=
@@ -765,7 +765,7 @@ noncomputable def cau_seq_abs (f : cau_seq ℂ abs) : cau_seq ℝ abs' :=
 lemma lim_abs (f : cau_seq ℂ abs) : lim (cau_seq_abs f) = abs (lim f) :=
 lim_eq_of_equiv_const (λ ε ε0,
 let ⟨i, hi⟩ := equiv_lim f ε ε0 in
-⟨i, λ j hj, lt_of_le_of_lt (abs_abs_sub_le_abs_sub _ _) (hi j hj)⟩)
+⟨i, λ j hj, lt_of_le_of_lt (abs.abs_abv_sub_le_abv_sub _ _) (hi j hj)⟩)
 
 variables {α : Type*} (s : finset α)
 
diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean
index 5d564c6b500b2..f6103c1abf302 100644
--- a/src/data/complex/exponential.lean
+++ b/src/data/complex/exponential.lean
@@ -313,16 +313,16 @@ namespace complex
 lemma is_cau_abs_exp (z : ℂ) : is_cau_seq has_abs.abs
   (λ n, ∑ m in range n, abs (z ^ m / m!)) :=
 let ⟨n, hn⟩ := exists_nat_gt (abs z) in
-have hn0 : (0 : ℝ) < n, from lt_of_le_of_lt (abs_nonneg _) hn,
-series_ratio_test n (complex.abs z / n) (div_nonneg (complex.abs_nonneg _) (le_of_lt hn0))
+have hn0 : (0 : ℝ) < n, from lt_of_le_of_lt (abs.nonneg _) hn,
+series_ratio_test n (complex.abs z / n) (div_nonneg (abs.nonneg _) (le_of_lt hn0))
   (by rwa [div_lt_iff hn0, one_mul])
   (λ m hm,
     by rw [abs_abs, abs_abs, nat.factorial_succ, pow_succ,
       mul_comm m.succ, nat.cast_mul, ← div_div, mul_div_assoc,
-      mul_div_right_comm, abs_mul, abs_div, abs_cast_nat];
+      mul_div_right_comm, abs.map_mul, map_div₀, abs_cast_nat];
     exact mul_le_mul_of_nonneg_right
-      (div_le_div_of_le_left (abs_nonneg _) hn0
-        (nat.cast_le.2 (le_trans hm (nat.le_succ _)))) (abs_nonneg _))
+      (div_le_div_of_le_left (abs.nonneg _) hn0
+        (nat.cast_le.2 (le_trans hm (nat.le_succ _)))) (abs.nonneg _))
 
 noncomputable theory
 
@@ -1296,17 +1296,17 @@ begin
   ... ≤ ∑ m in filter (λ k, n ≤ k) (range j), abs x ^ n * (1 / m!) :
     begin
       refine sum_le_sum (λ m hm, _),
-      rw [abs_mul, abv_pow abs, abs_div, abs_cast_nat],
+      rw [map_mul, map_pow, map_div₀, abs_cast_nat],
       refine mul_le_mul_of_nonneg_left ((div_le_div_right _).2 _) _,
       { exact nat.cast_pos.2 (nat.factorial_pos _), },
       { rw abv_pow abs,
-        exact (pow_le_one _ (abs_nonneg _) hx), },
-      { exact pow_nonneg (abs_nonneg _) _ },
+        exact (pow_le_one _ (abs.nonneg _) hx), },
+      { exact pow_nonneg (abs.nonneg _) _ },
     end
   ... = abs x ^ n * (∑ m in (range j).filter (λ k, n ≤ k), (1 / m! : ℝ)) :
     by simp [abs_mul, abv_pow abs, abs_div, mul_sum.symm]
   ... ≤ abs x ^ n * (n.succ * (n! * n)⁻¹) :
-    mul_le_mul_of_nonneg_left (sum_div_factorial_le _ _ hn) (pow_nonneg (abs_nonneg _) _)
+    mul_le_mul_of_nonneg_left (sum_div_factorial_le _ _ hn) (pow_nonneg (abs.nonneg _) _)
 end
 
 lemma exp_bound' {x : ℂ} {n : ℕ} (hx : abs x / (n.succ) ≤ 1 / 2) :
@@ -1322,11 +1322,11 @@ begin
   calc abs (∑ (i : ℕ) in range k, x ^ (n + i) / ((n + i)! : ℂ))
       ≤ ∑ (i : ℕ) in range k, abs (x ^ (n + i) / ((n + i)! : ℂ)) : abv_sum_le_sum_abv _ _
   ... ≤ ∑ (i : ℕ) in range k, (abs x) ^ (n + i) / (n + i)! :
-        by simp only [complex.abs_cast_nat, complex.abs_div, abv_pow abs]
+        by simp only [complex.abs_cast_nat, map_div₀, abv_pow abs]
   ... ≤ ∑ (i : ℕ) in range k, (abs x) ^ (n + i) / (n! * n.succ ^ i) : _
   ... = ∑ (i : ℕ) in range k, (abs x) ^ (n) / (n!) * ((abs x)^i / n.succ ^ i) : _
   ... ≤ abs x ^ n / (↑n!) * 2 : _,
-  { refine sum_le_sum (λ m hm, div_le_div (pow_nonneg (abs_nonneg x) (n + m)) le_rfl _ _),
+  { refine sum_le_sum (λ m hm, div_le_div (pow_nonneg (abs.nonneg x) (n + m)) le_rfl _ _),
     { exact_mod_cast mul_pos n.factorial_pos (pow_pos n.succ_pos _), },
     { exact_mod_cast (nat.factorial_mul_pow_le_factorial), }, },
   { refine finset.sum_congr rfl (λ _ _, _),
@@ -1338,11 +1338,11 @@ begin
       { transitivity (-1 : ℝ),
         { linarith },
         { simp only [neg_le_sub_iff_le_add, div_pow, nat.cast_succ, le_add_iff_nonneg_left],
-          exact div_nonneg (pow_nonneg (abs_nonneg x) k)
+          exact div_nonneg (pow_nonneg (abs.nonneg x) k)
             (pow_nonneg (add_nonneg n.cast_nonneg zero_le_one) k) } },
       { linarith },
       { linarith }, },
-    { exact div_nonneg (pow_nonneg (abs_nonneg x) n) (nat.cast_nonneg (n!)), }, },
+    { exact div_nonneg (pow_nonneg (abs.nonneg x) n) (nat.cast_nonneg (n!)), }, },
 end
 
 lemma abs_exp_sub_one_le {x : ℂ} (hx : abs x ≤ 1) :
@@ -1473,10 +1473,10 @@ calc |cos x - (1 - x ^ 2 / 2)| = abs (complex.cos x - (1 - x ^ 2 / 2)) :
   end)
 ... ≤ abs ((complex.exp (x * I) - ∑ m in range 4, (x * I) ^ m / m!) / 2) +
     abs ((complex.exp (-x * I) - ∑ m in range 4, (-x * I) ^ m / m!) / 2) :
-  by rw add_div; exact abs_add _ _
+  by rw add_div; exact complex.abs.add_le _ _
 ... = (abs ((complex.exp (x * I) - ∑ m in range 4, (x * I) ^ m / m!)) / 2 +
     abs ((complex.exp (-x * I) - ∑ m in range 4, (-x * I) ^ m / m!)) / 2) :
-  by simp [complex.abs_div]
+  by simp [map_div₀]
 ... ≤ ((complex.abs (x * I) ^ 4 * (nat.succ 4 * (4! * (4 : ℕ))⁻¹)) / 2 +
     (complex.abs (-x * I) ^ 4 * (nat.succ 4 * (4! * (4 : ℕ))⁻¹)) / 2)  :
   add_le_add ((div_le_div_right (by norm_num)).2 (complex.exp_bound (by simpa) dec_trivial))
@@ -1499,10 +1499,10 @@ calc |sin x - (x - x ^ 3 / 6)| = abs (complex.sin x - (x - x ^ 3 / 6)) :
   end)
 ... ≤ abs ((complex.exp (-x * I) - ∑ m in range 4, (-x * I) ^ m / m!) * I / 2) +
     abs (-((complex.exp (x * I) - ∑ m in range 4, (x * I) ^ m / m!) * I) / 2) :
-  by rw [sub_mul, sub_eq_add_neg, add_div]; exact abs_add _ _
+  by rw [sub_mul, sub_eq_add_neg, add_div]; exact complex.abs.add_le _ _
 ... = (abs ((complex.exp (x * I) - ∑ m in range 4, (x * I) ^ m / m!)) / 2 +
     abs ((complex.exp (-x * I) - ∑ m in range 4, (-x * I) ^ m / m!)) / 2) :
-  by simp [add_comm, complex.abs_div, complex.abs_mul]
+  by simp [add_comm, map_div₀]
 ... ≤ ((complex.abs (x * I) ^ 4 * (nat.succ 4 * (4! * (4 : ℕ))⁻¹)) / 2 +
     (complex.abs (-x * I) ^ 4 * (nat.succ 4 * (4! * (4 : ℕ))⁻¹)) / 2) :
   add_le_add ((div_le_div_right (by norm_num)).2 (complex.exp_bound (by simpa) dec_trivial))
@@ -1654,7 +1654,7 @@ by rw [← of_real_exp]; exact abs_of_nonneg (le_of_lt (real.exp_pos _))
 by rw [exp_mul_I, abs_cos_add_sin_mul_I]
 
 lemma abs_exp (z : ℂ) : abs (exp z) = real.exp z.re :=
-by rw [exp_eq_exp_re_mul_sin_add_cos, abs_mul, abs_exp_of_real, abs_cos_add_sin_mul_I, mul_one]
+by rw [exp_eq_exp_re_mul_sin_add_cos, map_mul, abs_exp_of_real, abs_cos_add_sin_mul_I, mul_one]
 
 lemma abs_exp_eq_iff_re_eq {x y : ℂ} : abs (exp x) = abs (exp y) ↔ x.re = y.re :=
 by rw [abs_exp, abs_exp, real.exp_eq_exp]
diff --git a/src/geometry/euclidean/oriented_angle.lean b/src/geometry/euclidean/oriented_angle.lean
index c803acefa02d3..580adeea1ba38 100644
--- a/src/geometry/euclidean/oriented_angle.lean
+++ b/src/geometry/euclidean/oriented_angle.lean
@@ -869,7 +869,7 @@ begin
   by_cases hx : x = 0, { simp [hx] },
   by_cases hy : y = 0, { simp [hy] },
   rw [oangle, real.angle.cos_coe, complex.cos_arg], swap, { simp [hx, hy] },
-  simp_rw [complex.abs_div, ←complex.norm_eq_abs, linear_isometry_equiv.norm_map, complex.div_re,
+  simp_rw [map_div₀, ←complex.norm_eq_abs, linear_isometry_equiv.norm_map, complex.div_re,
            ←complex.sq_abs, ←complex.norm_eq_abs, linear_isometry_equiv.norm_map,
            complex.isometry_of_orthonormal_symm_apply, complex.add_re, complex.add_im,
            is_R_or_C.I, complex.mul_I_re, complex.mul_I_im, complex.of_real_re,
diff --git a/src/measure_theory/integral/circle_integral.lean b/src/measure_theory/integral/circle_integral.lean
index 111cfaef670a9..be24aaf99983c 100644
--- a/src/measure_theory/integral/circle_integral.lean
+++ b/src/measure_theory/integral/circle_integral.lean
@@ -268,12 +268,17 @@ begin
           (deriv_circle_map_ne_zero hR)).eventually this,
       filter_upwards [self_mem_nhds_within,
         mem_nhds_within_of_mem_nhds (ball_mem_nhds _ zero_lt_one)],
-      simp [dist_eq, sub_eq_zero] { contextual := tt } },
+      simp only [dist_eq, sub_eq_zero, mem_compl_iff, mem_singleton_iff, mem_ball, mem_diff,
+                 mem_ball_zero_iff, norm_eq_abs, not_false_iff, and_self, implies_true_iff]
+                {contextual := tt} },
     refine ((((has_deriv_at_circle_map c R θ).is_O_sub).mono inf_le_left).inv_rev
       (this.mono (λ θ' h₁ h₂, absurd h₂ h₁.2))).trans _,
     refine is_O.of_bound (|R|)⁻¹ (this.mono $ λ θ' hθ', _),
     set x := abs (f θ'),
-    suffices : x⁻¹ ≤ x ^ n, by simpa [inv_mul_cancel_left₀, mt _root_.abs_eq_zero.1 hR],
+    suffices : x⁻¹ ≤ x ^ n,
+    by simpa only [inv_mul_cancel_left₀, abs_eq_zero.not.2 hR, norm_eq_abs, map_inv₀,
+                   algebra.id.smul_eq_mul, map_mul, abs_circle_map_zero, abs_I, mul_one,
+                   abs_zpow, ne.def, not_false_iff] using this,
     have : x ∈ Ioo (0 : ℝ) 1, by simpa [and.comm, x] using hθ',
     rw ← zpow_neg_one,
     refine (zpow_strict_anti this.1 this.2).le_iff_le.2 (int.lt_add_one_iff.1 _), exact hn },
@@ -371,7 +376,7 @@ begin
     interval_integral.norm_integral_le_integral_norm real.two_pi_pos.le
   ... < ∫ θ in 0..2 * π, R * C :
     begin
-      simp only [norm_smul, deriv_circle_map, norm_eq_abs, complex.abs_mul, abs_I, mul_one,
+      simp only [norm_smul, deriv_circle_map, norm_eq_abs, map_mul, abs_I, mul_one,
         abs_circle_map_zero, abs_of_pos hR],
       refine interval_integral.integral_lt_integral_of_continuous_on_of_le_of_exists_lt
         real.two_pi_pos _ continuous_on_const (λ θ hθ, _) ⟨θ₀, Ioc_subset_Icc_self hmem, _⟩,
@@ -513,9 +518,9 @@ lemma has_sum_two_pi_I_cauchy_power_series_integral {f : ℂ → E} {c : ℂ} {R
   has_sum (λ n : ℕ, ∮ z in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
     (∮ z in C(c, R), (z - (c + w))⁻¹ • f z) :=
 begin
-  have hR : 0 < R := (abs_nonneg w).trans_lt hw,
+  have hR : 0 < R := (complex.abs.nonneg w).trans_lt hw,
   have hwR : abs w / R ∈ Ico (0 : ℝ) 1,
-    from ⟨div_nonneg (abs_nonneg w) hR.le, (div_lt_one hR).2 hw⟩,
+    from ⟨div_nonneg (complex.abs.nonneg w) hR.le, (div_lt_one hR).2 hw⟩,
   refine interval_integral.has_sum_integral_of_dominated_convergence
     (λ n θ, ∥f (circle_map c R θ)∥ * (abs w / R) ^ n) (λ n, _) (λ n, _) _ _ _,
   { simp only [deriv_circle_map],
diff --git a/src/measure_theory/integral/circle_transform.lean b/src/measure_theory/integral/circle_transform.lean
index 36b42bcf906b1..7086f0aef089c 100644
--- a/src/measure_theory/integral/circle_transform.lean
+++ b/src/measure_theory/integral/circle_transform.lean
@@ -160,10 +160,11 @@ begin
   have hy2: y1 ∈ [0, 2*π], by {convert (Ico_subset_Icc_self hy1),
     simp [interval_of_le real.two_pi_pos.le]},
   have := mul_le_mul (hab ⟨⟨v, y1⟩, ⟨ball_subset_closed_ball (H hv), hy2⟩⟩)
-   (HX2 (circle_map z R y1) (circle_map_mem_sphere z hR.le y1)) (abs_nonneg _) (abs_nonneg _),
-   simp_rw hfun,
+   (HX2 (circle_map z R y1) (circle_map_mem_sphere z hR.le y1))
+   (complex.abs.nonneg _) (complex.abs.nonneg _),
+  simp_rw hfun,
   simp only [circle_transform_bounding_function, circle_transform_deriv, V, norm_eq_abs,
-    algebra.id.smul_eq_mul, deriv_circle_map, abs_mul, abs_circle_map_zero, abs_I, mul_one,
+    algebra.id.smul_eq_mul, deriv_circle_map, map_mul, abs_circle_map_zero, abs_I, mul_one,
     ←mul_assoc, mul_inv_rev, inv_I, abs_neg, abs_inv, abs_of_real, one_mul, abs_two, abs_pow,
     mem_ball, gt_iff_lt, subtype.coe_mk, set_coe.forall, mem_prod, mem_closed_ball, and_imp,
     prod.forall, normed_space.sphere_nonempty, mem_sphere_iff_norm] at *,
diff --git a/src/number_theory/l_series.lean b/src/number_theory/l_series.lean
index b010d326c6b85..47fd7d2cd9d66 100644
--- a/src/number_theory/l_series.lean
+++ b/src/number_theory/l_series.lean
@@ -52,17 +52,17 @@ theorem l_series_summable_of_bounded_of_one_lt_real {f : arithmetic_function ℂ
 begin
   by_cases h0 : m = 0,
   { subst h0,
-    have hf : f = 0 := arithmetic_function.ext (λ n, complex.abs_eq_zero.1
-        (le_antisymm (h n) (complex.abs_nonneg _))),
+    have hf : f = 0 := arithmetic_function.ext (λ n, complex.abs.eq_zero.1
+        (le_antisymm (h n) (complex.abs.nonneg _))),
     simp [hf] },
   refine summable_of_norm_bounded (λ (n : ℕ), m / (n ^ z)) _ _,
   { simp_rw [div_eq_mul_inv],
     exact (summable_mul_left_iff h0).1 (real.summable_nat_rpow_inv.2 hz) },
   { intro n,
-    have hm : 0 ≤ m := le_trans (complex.abs_nonneg _) (h 0),
+    have hm : 0 ≤ m := le_trans (complex.abs.nonneg _) (h 0),
     cases n,
     { simp [hm, real.zero_rpow (ne_of_gt (lt_trans real.zero_lt_one hz))] },
-    simp only [complex.abs_div, complex.norm_eq_abs],
+    simp only [map_div₀, complex.norm_eq_abs],
     apply div_le_div hm (h _) (real.rpow_pos_of_pos (nat.cast_pos.2 n.succ_pos) _) (le_of_eq _),
     rw [complex.abs_cpow_real, complex.abs_cast_nat] }
 end
@@ -109,10 +109,11 @@ begin
     ext n,
     simp [n.succ_ne_zero] },
   { apply congr rfl,
-    ext n,
-    cases n, { simp [h0] },
-    simp only [n.succ_ne_zero, one_div, cast_one, nat_coe_apply, complex.abs_cpow_real, inv_inj,
-      complex.abs_inv, if_false, zeta_apply, complex.norm_eq_abs, complex.abs_of_nat] }
+    ext ⟨-|n⟩,
+    { simp [h0] },
+    simp only [cast_zero, nat_coe_apply, zeta_apply, succ_ne_zero, if_false, cast_succ, one_div,
+               complex.norm_eq_abs, map_inv₀, complex.abs_cpow_real, inv_inj, zero_add],
+    rw [←cast_one, ←cast_add, complex.abs_of_nat, cast_add, cast_one] }
 end
 
 @[simp] theorem l_series_add {f g : arithmetic_function ℂ} {z : ℂ}
diff --git a/src/number_theory/modular.lean b/src/number_theory/modular.lean
index d8ecd9a6ea780..8a66693a5ff4c 100644
--- a/src/number_theory/modular.lean
+++ b/src/number_theory/modular.lean
@@ -62,7 +62,7 @@ we state lemmas in this file without spurious `coe_fn` terms. -/
 local attribute [-instance] matrix.special_linear_group.has_coe_to_fun
 local attribute [-instance] matrix.general_linear_group.has_coe_to_fun
 
-open complex (hiding abs_one abs_two abs_mul abs_add)
+open complex (hiding abs_two)
 open matrix (hiding mul_smul) matrix.special_linear_group upper_half_plane
 noncomputable theory
 
diff --git a/src/ring_theory/polynomial/cyclotomic/eval.lean b/src/ring_theory/polynomial/cyclotomic/eval.lean
index 79c5b3ed040c4..8cd844817de6a 100644
--- a/src/ring_theory/polynomial/cyclotomic/eval.lean
+++ b/src/ring_theory/polynomial/cyclotomic/eval.lean
@@ -199,7 +199,7 @@ begin
   { refine ⟨ζ, (mem_primitive_roots hn).mpr hζ, _⟩,
     suffices : ¬ same_ray ℝ (q : ℂ) ζ,
     { convert lt_norm_sub_of_not_same_ray this;
-      simp [real.norm_of_nonneg hq.le, hζ.norm'_eq_one hn.ne'] },
+      simp only [hζ.norm'_eq_one hn.ne', real.norm_of_nonneg hq.le, complex.norm_real] },
     rw complex.same_ray_iff,
     push_neg,
     refine ⟨by exact_mod_cast hq.ne', hζ.ne_zero hn.ne', _⟩,
@@ -209,7 +209,8 @@ begin
     linarith [hζ.unique is_primitive_root.one] },
   have : ¬eval ↑q (cyclotomic n ℂ) = 0,
   { erw cyclotomic.eval_apply q n (algebra_map ℝ ℂ),
-    simpa using (cyclotomic_pos' n hq').ne' },
+    simpa only [complex.coe_algebra_map, complex.of_real_eq_zero]
+                using (cyclotomic_pos' n hq').ne' },
   suffices : (units.mk0 (real.to_nnreal (q - 1)) (by simp [hq'])) ^ totient n
               < units.mk0 (∥(cyclotomic n ℂ).eval q∥₊) (by simp [this]),
   { simp only [←units.coe_lt_coe, units.coe_pow, units.coe_mk0, ← nnreal.coe_lt_coe, hq'.le,
@@ -217,20 +218,21 @@ begin
                nnreal.coe_pow, real.coe_to_nnreal', max_eq_left, sub_nonneg] at this,
     convert this,
     erw [(cyclotomic.eval_apply q n (algebra_map ℝ ℂ)), eq_comm],
-    simp [cyclotomic_nonneg n hq'.le], },
+    simp only [cyclotomic_nonneg n hq'.le, complex.coe_algebra_map,
+               complex.abs_of_real, abs_eq_self], },
   simp only [cyclotomic_eq_prod_X_sub_primitive_roots hζ, eval_prod, eval_C,
              eval_X, eval_sub, nnnorm_prod, units.mk0_prod],
   convert finset.prod_lt_prod' _ _,
   swap, { exact λ _, units.mk0 (real.to_nnreal (q - 1)) (by simp [hq']) },
-  { simp [complex.card_primitive_roots] },
+  { simp only [complex.card_primitive_roots, prod_const, card_attach] },
   { simp only [subtype.coe_mk, finset.mem_attach, forall_true_left, subtype.forall,
-      ←units.coe_le_coe, ← nnreal.coe_le_coe, complex.abs_nonneg, hq'.le, units.coe_mk0,
+      ←units.coe_le_coe, ← nnreal.coe_le_coe, complex.abs.nonneg, hq'.le, units.coe_mk0,
       real.coe_to_nnreal', coe_nnnorm, complex.norm_eq_abs, max_le_iff, tsub_le_iff_right],
     intros x hx,
-    simpa using hfor x hx, },
+    simpa only [and_true, tsub_le_iff_right] using hfor x hx, },
   { simp only [subtype.coe_mk, finset.mem_attach, exists_true_left, subtype.exists,
       ← nnreal.coe_lt_coe, ← units.coe_lt_coe, units.coe_mk0 _, coe_nnnorm],
-    simpa [hq'.le] using hex, },
+    simpa only [hq'.le, real.coe_to_nnreal', max_eq_left, sub_nonneg] using hex },
 end
 
 lemma cyclotomic_eval_lt_sub_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤ n) (hq' : 1 < q) :
@@ -287,7 +289,7 @@ begin
   swap, { exact λ _, units.mk0 (real.to_nnreal (q + 1)) (by simp; linarith only [hq']) },
   { simp [complex.card_primitive_roots], },
   { simp only [subtype.coe_mk, finset.mem_attach, forall_true_left, subtype.forall,
-      ←units.coe_le_coe, ← nnreal.coe_le_coe, complex.abs_nonneg, hq'.le, units.coe_mk0,
+      ←units.coe_le_coe, ← nnreal.coe_le_coe, complex.abs.nonneg, hq'.le, units.coe_mk0,
       real.coe_to_nnreal, coe_nnnorm, complex.norm_eq_abs, max_le_iff],
     intros x hx,
     have : complex.abs _ ≤ _ := hfor x hx,