From cc1fdf36ced4e3b7a957b0142a68ccd2ca770a83 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Fri, 18 Jun 2021 11:58:44 +0200
Subject: [PATCH 1/9] add has_nndist

---
 src/topology/metric_space/basic.lean | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
index 3d9f7e5dcd357..896b404eecc3c 100644
--- a/src/topology/metric_space/basic.lean
+++ b/src/topology/metric_space/basic.lean
@@ -191,8 +191,14 @@ nonneg_of_mul_nonneg_left this zero_lt_two
 @[simp] theorem abs_dist {a b : α} : abs (dist a b) = dist a b :=
 abs_of_nonneg dist_nonneg
 
+/-- A version of `has_dist` that takes value in `ℝ≥0`. -/
+class has_nndist (α : Type*) := (nndist : α → α → ℝ≥0)
+
+export has_nndist (nndist)
+
+
 /-- Distance as a nonnegative real number. -/
-def nndist (a b : α) : ℝ≥0 := ⟨dist a b, dist_nonneg⟩
+instance nndist_of_pseudo_metric_space : has_nndist α := ⟨λ a b, ⟨dist a b, dist_nonneg⟩⟩
 
 /--Express `nndist` in terms of `edist`-/
 lemma nndist_edist (x y : α) : nndist x y = (edist x y).to_nnreal :=
@@ -200,7 +206,7 @@ by simp [nndist, edist_dist, real.to_nnreal, max_eq_left dist_nonneg, ennreal.of
 
 /--Express `edist` in terms of `nndist`-/
 lemma edist_nndist (x y : α) : edist x y = ↑(nndist x y) :=
-by { rw [edist_dist, nndist, ennreal.of_real_eq_coe_nnreal] }
+by { rw [edist_dist, ennreal.of_real_eq_coe_nnreal dist_nonneg], refl }
 
 @[simp, norm_cast] lemma coe_nnreal_ennreal_nndist (x y : α) : ↑(nndist x y) = edist x y :=
 (edist_nndist x y).symm

From 028c891c3548b1f39311d1d47fc613fc15b21224 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Fri, 18 Jun 2021 12:42:37 +0200
Subject: [PATCH 2/9] better name

---
 src/topology/metric_space/basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
index 896b404eecc3c..4529de3540b1e 100644
--- a/src/topology/metric_space/basic.lean
+++ b/src/topology/metric_space/basic.lean
@@ -198,7 +198,7 @@ export has_nndist (nndist)
 
 
 /-- Distance as a nonnegative real number. -/
-instance nndist_of_pseudo_metric_space : has_nndist α := ⟨λ a b, ⟨dist a b, dist_nonneg⟩⟩
+instance pseudo_metric_space.to_has_nndist : has_nndist α := ⟨λ a b, ⟨dist a b, dist_nonneg⟩⟩
 
 /--Express `nndist` in terms of `edist`-/
 lemma nndist_edist (x y : α) : nndist x y = (edist x y).to_nnreal :=

From 9f0bd6931f76147a2cc8fdf5a4b532f8f607e4f4 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Fri, 18 Jun 2021 13:36:39 +0200
Subject: [PATCH 3/9] golf

---
 src/topology/metric_space/basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
index 4529de3540b1e..92bf8aa294802 100644
--- a/src/topology/metric_space/basic.lean
+++ b/src/topology/metric_space/basic.lean
@@ -206,7 +206,7 @@ by simp [nndist, edist_dist, real.to_nnreal, max_eq_left dist_nonneg, ennreal.of
 
 /--Express `edist` in terms of `nndist`-/
 lemma edist_nndist (x y : α) : edist x y = ↑(nndist x y) :=
-by { rw [edist_dist, ennreal.of_real_eq_coe_nnreal dist_nonneg], refl }
+by { simpa only [edist_dist, ennreal.of_real_eq_coe_nnreal dist_nonneg] }
 
 @[simp, norm_cast] lemma coe_nnreal_ennreal_nndist (x y : α) : ↑(nndist x y) = edist x y :=
 (edist_nndist x y).symm

From 287e817cd2c87e52830167a80d10aba5759351ff Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Fri, 18 Jun 2021 13:36:50 +0200
Subject: [PATCH 4/9] add has_nnnorm

---
 src/analysis/normed_space/basic.lean | 108 ++++++++++++++-------------
 1 file changed, 57 insertions(+), 51 deletions(-)

diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index a8f1b74ac15ab..5b3f862a36864 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -359,35 +359,41 @@ lemma add_monoid_hom.continuous_of_bound (f : α →+ β) (C : ℝ) (h : ∀x, 
 
 section nnnorm
 
-/-- Version of the norm taking values in nonnegative reals. -/
-def nnnorm (a : α) : ℝ≥0 := ⟨norm a, norm_nonneg a⟩
+/-- Auxiliary class, endowing a type `α` with a function `nnnorm : α → ℝ≥0`. -/
+class has_nnnorm (α : Type*) := (nnnorm : α → ℝ≥0)
 
-@[simp, norm_cast] lemma coe_nnnorm (a : α) : (nnnorm a : ℝ) = norm a := rfl
+export has_nnnorm (nnnorm)
 
-lemma nndist_eq_nnnorm (a b : α) : nndist a b = nnnorm (a - b) := nnreal.eq $ dist_eq_norm _ _
+notation `∥₊`:1024 e:1 `∥`:1 := nnnorm e
 
-@[simp] lemma nnnorm_zero : nnnorm (0 : α) = 0 :=
+instance semi_normed_group.to_has_nnnorm : has_nnnorm α := ⟨λ a, ⟨norm a, norm_nonneg a⟩⟩
+
+@[simp, norm_cast] lemma coe_nnnorm (a : α) : (∥₊a∥ : ℝ) = norm a := rfl
+
+lemma nndist_eq_nnnorm (a b : α) : nndist a b = ∥₊a - b∥ := nnreal.eq $ dist_eq_norm _ _
+
+@[simp] lemma nnnorm_zero : ∥₊(0 : α)∥ = 0 :=
 nnreal.eq norm_zero
 
-lemma nnnorm_add_le (g h : α) : nnnorm (g + h) ≤ nnnorm g + nnnorm h :=
+lemma nnnorm_add_le (g h : α) : ∥₊g + h∥ ≤ ∥₊g∥ + ∥₊h∥ :=
 nnreal.coe_le_coe.2 $ norm_add_le g h
 
-@[simp] lemma nnnorm_neg (g : α) : nnnorm (-g) = nnnorm g :=
+@[simp] lemma nnnorm_neg (g : α) : ∥₊-g∥ = ∥₊g∥ :=
 nnreal.eq $ norm_neg g
 
-lemma nndist_nnnorm_nnnorm_le (g h : α) : nndist (nnnorm g) (nnnorm h) ≤ nnnorm (g - h) :=
+lemma nndist_nnnorm_nnnorm_le (g h : α) : nndist ∥₊g∥ ∥₊h∥ ≤ ∥₊g - h∥ :=
 nnreal.coe_le_coe.2 $ dist_norm_norm_le g h
 
-lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (nnnorm x : ℝ≥0∞) :=
+lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (∥₊x∥ : ℝ≥0∞) :=
 ennreal.of_real_eq_coe_nnreal _
 
-lemma edist_eq_coe_nnnorm_sub (x y : β) : edist x y = (nnnorm (x - y) : ℝ≥0∞) :=
+lemma edist_eq_coe_nnnorm_sub (x y : β) : edist x y = (∥₊x - y∥ : ℝ≥0∞) :=
 by rw [edist_dist, dist_eq_norm, of_real_norm_eq_coe_nnnorm]
 
-lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (nnnorm x : ℝ≥0∞) :=
+lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (∥₊x∥ : ℝ≥0∞) :=
 by rw [edist_eq_coe_nnnorm_sub, _root_.sub_zero]
 
-lemma mem_emetric_ball_0_iff {x : β} {r : ℝ≥0∞} : x ∈ emetric.ball (0 : β) r ↔ ↑(nnnorm x) < r :=
+lemma mem_emetric_ball_0_iff {x : β} {r : ℝ≥0∞} : x ∈ emetric.ball (0 : β) r ↔ ↑∥₊x∥ < r :=
 by rw [emetric.mem_ball, edist_eq_coe_nnnorm]
 
 lemma nndist_add_add_le (g₁ g₂ h₁ h₂ : α) :
@@ -399,7 +405,7 @@ lemma edist_add_add_le (g₁ g₂ h₁ h₂ : α) :
 by { simp only [edist_nndist], norm_cast, apply nndist_add_add_le }
 
 lemma nnnorm_sum_le {β} : ∀(s : finset β) (f : β → α),
-  nnnorm (∑ a in s, f a) ≤ ∑ a in s, nnnorm (f a) :=
+  ∥₊∑ a in s, f a∥ ≤ ∑ a in s, ∥₊f a∥ :=
 finset.le_sum_of_subadditive nnnorm nnnorm_zero nnnorm_add_le
 
 end nnnorm
@@ -485,7 +491,7 @@ instance prod.semi_normed_group : semi_normed_group (α × β) :=
 
 lemma prod.semi_norm_def (x : α × β) : ∥x∥ = (max ∥x.1∥ ∥x.2∥) := rfl
 
-lemma prod.nnsemi_norm_def (x : α × β) : nnnorm x = max (nnnorm x.1) (nnnorm x.2) :=
+lemma prod.nnsemi_norm_def (x : α × β) : ∥₊x∥ = max ∥₊x.1∥ ∥₊x.2∥ :=
 by { have := x.semi_norm_def, simp only [← coe_nnnorm] at this, exact_mod_cast this }
 
 lemma semi_norm_fst_le (x : α × β) : ∥x.1∥ ≤ ∥x∥ :=
@@ -502,10 +508,10 @@ max_le_iff
 using the sup norm. -/
 instance pi.semi_normed_group {π : ι → Type*} [fintype ι] [∀i, semi_normed_group (π i)] :
   semi_normed_group (Πi, π i) :=
-{ norm := λf, ((finset.sup finset.univ (λ b, nnnorm (f b)) : ℝ≥0) : ℝ),
+{ norm := λf, ((finset.sup finset.univ (λ b, ∥₊f b∥) : ℝ≥0) : ℝ),
   dist_eq := assume x y,
     congr_arg (coe : ℝ≥0 → ℝ) $ congr_arg (finset.sup finset.univ) $ funext $ assume a,
-    show nndist (x a) (y a) = nnnorm (x a - y a), from nndist_eq_nnnorm _ _ }
+    show nndist (x a) (y a) = ∥₊x a - y a∥, from nndist_eq_nnnorm _ _ }
 
 /-- The seminorm of an element in a product space is `≤ r` if and only if the norm of each
 component is. -/
@@ -527,7 +533,7 @@ lemma semi_norm_le_pi_norm {π : ι → Type*} [fintype ι] [∀i, semi_normed_g
 by simpa only [← dist_zero_right] using dist_pi_const a 0
 
 @[simp] lemma pi_nnsemi_norm_const [nonempty ι] [fintype ι] (a : α) :
-  nnnorm (λ i : ι, a) = nnnorm a :=
+  ∥₊(λ i : ι, a)∥ = ∥₊a∥ :=
 nnreal.eq $ pi_semi_norm_const a
 
 lemma tendsto_iff_norm_tendsto_zero {f : ι → β} {a : filter ι} {b : β} :
@@ -577,7 +583,7 @@ lemma continuous_norm : continuous (λg:α, ∥g∥) :=
 by simpa using continuous_id.dist (continuous_const : continuous (λ g, (0:α)))
 
 @[continuity]
-lemma continuous_nnnorm : continuous (nnnorm : α → ℝ≥0) :=
+lemma continuous_nnnorm : continuous (λ (a : α), ∥₊a∥) :=
 continuous_subtype_mk _ continuous_norm
 
 lemma lipschitz_with_one_norm : lipschitz_with 1 (norm : α → ℝ) :=
@@ -586,7 +592,7 @@ by simpa only [dist_zero_left] using lipschitz_with.dist_right (0 : α)
 lemma uniform_continuous_norm : uniform_continuous (norm : α → ℝ) :=
 lipschitz_with_one_norm.uniform_continuous
 
-lemma uniform_continuous_nnnorm : uniform_continuous (nnnorm : α → ℝ≥0) :=
+lemma uniform_continuous_nnnorm : uniform_continuous (λ (a : α), ∥₊a∥) :=
 uniform_continuous_subtype_mk uniform_continuous_norm _
 
 section
@@ -597,7 +603,7 @@ lemma filter.tendsto.norm {a : α} (h : tendsto f l (𝓝 a)) : tendsto (λ x, 
 tendsto_norm.comp h
 
 lemma filter.tendsto.nnnorm (h : tendsto f l (𝓝 a)) :
-  tendsto (λ x, nnnorm (f x)) l (𝓝 (nnnorm a)) :=
+  tendsto (λ x, ∥₊f x∥) l (𝓝 (∥₊a∥)) :=
 tendsto.comp continuous_nnnorm.continuous_at h
 
 end
@@ -608,25 +614,25 @@ variables [topological_space γ] {f : γ → α} {s : set γ} {a : γ} {b : α}
 
 lemma continuous.norm (h : continuous f) : continuous (λ x, ∥f x∥) := continuous_norm.comp h
 
-lemma continuous.nnnorm (h : continuous f) : continuous (λ x, nnnorm (f x)) :=
+lemma continuous.nnnorm (h : continuous f) : continuous (λ x, ∥₊f x∥) :=
 continuous_nnnorm.comp h
 
 lemma continuous_at.norm (h : continuous_at f a) : continuous_at (λ x, ∥f x∥) a := h.norm
 
-lemma continuous_at.nnnorm (h : continuous_at f a) : continuous_at (λ x, nnnorm (f x)) a := h.nnnorm
+lemma continuous_at.nnnorm (h : continuous_at f a) : continuous_at (λ x, ∥₊f x∥) a := h.nnnorm
 
 lemma continuous_within_at.norm (h : continuous_within_at f s a) :
   continuous_within_at (λ x, ∥f x∥) s a :=
 h.norm
 
 lemma continuous_within_at.nnnorm (h : continuous_within_at f s a) :
-  continuous_within_at (λ x, nnnorm (f x)) s a :=
+  continuous_within_at (λ x, ∥₊f x∥) s a :=
 h.nnnorm
 
 lemma continuous_on.norm (h : continuous_on f s) : continuous_on (λ x, ∥f x∥) s :=
 λ x hx, (h x hx).norm
 
-lemma continuous_on.nnnorm (h : continuous_on f s) : continuous_on (λ x, nnnorm (f x)) s :=
+lemma continuous_on.nnnorm (h : continuous_on f s) : continuous_on (λ x, ∥₊f x∥) s :=
 λ x hx, (h x hx).nnnorm
 
 end
@@ -754,7 +760,7 @@ begin
   rwa dist_eq_norm
 end
 
-@[simp] lemma nnnorm_eq_zero {a : α} : nnnorm a = 0 ↔ a = 0 :=
+@[simp] lemma nnnorm_eq_zero {a : α} : ∥₊a∥ = 0 ↔ a = 0 :=
 by simp only [nnreal.eq_iff.symm, nnreal.coe_zero, coe_nnnorm, norm_eq_zero]
 
 /-- A subgroup of a normed group is also a normed group, with the restriction of the norm. -/
@@ -774,7 +780,7 @@ instance prod.normed_group : normed_group (α × β) := { ..prod.semi_normed_gro
 
 lemma prod.norm_def (x : α × β) : ∥x∥ = (max ∥x.1∥ ∥x.2∥) := rfl
 
-lemma prod.nnnorm_def (x : α × β) : nnnorm x = max (nnnorm x.1) (nnnorm x.2) :=
+lemma prod.nnnorm_def (x : α × β) : ∥₊x∥ = max ∥₊x.1∥ ∥₊x.2∥ :=
 by { have := x.norm_def, simp only [← coe_nnnorm] at this, exact_mod_cast this }
 
 lemma norm_fst_le (x : α × β) : ∥x.1∥ ≤ ∥x∥ :=
@@ -811,7 +817,7 @@ lemma norm_le_pi_norm {π : ι → Type*} [fintype ι] [∀i, normed_group (π i
 by simpa only [← dist_zero_right] using dist_pi_const a 0
 
 @[simp] lemma pi_nnnorm_const [nonempty ι] [fintype ι] (a : α) :
-  nnnorm (λ i : ι, a) = nnnorm a :=
+  ∥₊(λ i : ι, a)∥ = ∥₊a∥ :=
 nnreal.eq $ pi_norm_const a
 
 lemma tendsto_norm_nhds_within_zero : tendsto (norm : α → ℝ) (𝓝[{0}ᶜ] 0) (𝓝[set.Ioi 0] 0) :=
@@ -867,7 +873,7 @@ export norm_one_class (norm_one)
 
 attribute [simp] norm_one
 
-@[simp] lemma nnnorm_one [semi_normed_group α] [has_one α] [norm_one_class α] : nnnorm (1:α) = 1 :=
+@[simp] lemma nnnorm_one [semi_normed_group α] [has_one α] [norm_one_class α] : ∥₊(1:α)∥ = 1 :=
 nnreal.eq norm_one
 
 @[priority 100] -- see Note [lower instance priority]
@@ -1047,7 +1053,7 @@ instance to_norm_one_class : norm_one_class α :=
 ⟨mul_left_cancel' (mt norm_eq_zero.1 (@one_ne_zero α _ _)) $
   by rw [← norm_mul, mul_one, mul_one]⟩
 
-@[simp] lemma nnnorm_mul (a b : α) : nnnorm (a * b) = nnnorm a * nnnorm b :=
+@[simp] lemma nnnorm_mul (a b : α) : ∥₊a * b∥ = ∥₊a∥ * ∥₊b∥ :=
 nnreal.eq $ norm_mul a b
 
 /-- `norm` as a `monoid_hom`. -/
@@ -1060,7 +1066,7 @@ nnreal.eq $ norm_mul a b
 @[simp] lemma norm_pow (a : α) : ∀ (n : ℕ), ∥a ^ n∥ = ∥a∥ ^ n :=
 (norm_hom.to_monoid_hom : α →* ℝ).map_pow a
 
-@[simp] lemma nnnorm_pow (a : α) (n : ℕ) : nnnorm (a ^ n) = nnnorm a ^ n :=
+@[simp] lemma nnnorm_pow (a : α) (n : ℕ) : ∥₊a ^ n∥ = ∥₊a∥ ^ n :=
 (nnnorm_hom.to_monoid_hom : α →* ℝ≥0).map_pow a n
 
 @[simp] lemma norm_prod (s : finset β) (f : β → α) :
@@ -1068,25 +1074,25 @@ nnreal.eq $ norm_mul a b
 (norm_hom.to_monoid_hom : α →* ℝ).map_prod f s
 
 @[simp] lemma nnnorm_prod (s : finset β) (f : β → α) :
-  nnnorm (∏ b in s, f b) = ∏ b in s, nnnorm (f b) :=
+  ∥₊∏ b in s, f b∥ = ∏ b in s, ∥₊f b∥ :=
 (nnnorm_hom.to_monoid_hom : α →* ℝ≥0).map_prod f s
 
 @[simp] lemma norm_div (a b : α) : ∥a / b∥ = ∥a∥ / ∥b∥ :=
 (norm_hom : monoid_with_zero_hom α ℝ).map_div a b
 
-@[simp] lemma nnnorm_div (a b : α) : nnnorm (a / b) = nnnorm a / nnnorm b :=
+@[simp] lemma nnnorm_div (a b : α) : ∥₊a / b∥ = ∥₊a∥ / ∥₊b∥ :=
 (nnnorm_hom : monoid_with_zero_hom α ℝ≥0).map_div a b
 
 @[simp] lemma norm_inv (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ :=
 (norm_hom : monoid_with_zero_hom α ℝ).map_inv' a
 
-@[simp] lemma nnnorm_inv (a : α) : nnnorm (a⁻¹) = (nnnorm a)⁻¹ :=
+@[simp] lemma nnnorm_inv (a : α) : ∥₊a⁻¹∥ = ∥₊a∥⁻¹ :=
 nnreal.eq $ by simp
 
 @[simp] lemma norm_fpow : ∀ (a : α) (n : ℤ), ∥a^n∥ = ∥a∥^n :=
 (norm_hom : monoid_with_zero_hom α ℝ).map_fpow
 
-@[simp] lemma nnnorm_fpow : ∀ (a : α) (n : ℤ), nnnorm (a^n) = (nnnorm a)^n :=
+@[simp] lemma nnnorm_fpow : ∀ (a : α) (n : ℤ), ∥₊a ^ n∥ = ∥₊a∥ ^ n :=
 (nnnorm_hom : monoid_with_zero_hom α ℝ≥0).map_fpow
 
 @[priority 100] -- see Note [lower instance priority]
@@ -1167,16 +1173,16 @@ abs_of_nonneg hx
 
 @[simp] lemma norm_coe_nat (n : ℕ) : ∥(n : ℝ)∥ = n := abs_of_nonneg n.cast_nonneg
 
-@[simp] lemma nnnorm_coe_nat (n : ℕ) : nnnorm (n : ℝ) = n := nnreal.eq $ by simp
+@[simp] lemma nnnorm_coe_nat (n : ℕ) : ∥₊(n : ℝ)∥ = n := nnreal.eq $ by simp
 
-@[simp] lemma norm_two : ∥(2:ℝ)∥ = 2 := abs_of_pos (@zero_lt_two ℝ _ _)
+@[simp] lemma norm_two : ∥(2 : ℝ)∥ = 2 := abs_of_pos (@zero_lt_two ℝ _ _)
 
-@[simp] lemma nnnorm_two : nnnorm (2:ℝ) = 2 := nnreal.eq $ by simp
+@[simp] lemma nnnorm_two : ∥₊(2 : ℝ)∥ = 2 := nnreal.eq $ by simp
 
-lemma nnnorm_of_nonneg {x : ℝ} (hx : 0 ≤ x) : nnnorm x = ⟨x, hx⟩ :=
+lemma nnnorm_of_nonneg {x : ℝ} (hx : 0 ≤ x) : ∥₊x∥ = ⟨x, hx⟩ :=
 nnreal.eq $ norm_of_nonneg hx
 
-lemma ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) : (nnnorm x : ℝ≥0∞) = ennreal.of_real x :=
+lemma ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) : (∥₊x∥ : ℝ≥0∞) = ennreal.of_real x :=
 by { rw [← of_real_norm_eq_coe_nnnorm, norm_of_nonneg hx] }
 
 end real
@@ -1188,7 +1194,7 @@ open_locale nnreal
 @[simp] lemma norm_eq (x : ℝ≥0) : ∥(x : ℝ)∥ = x :=
 by rw [real.norm_eq_abs, x.abs_eq]
 
-@[simp] lemma nnnorm_eq (x : ℝ≥0) : nnnorm (x : ℝ) = x :=
+@[simp] lemma nnnorm_eq (x : ℝ≥0) : ∥₊(x : ℝ)∥ = x :=
 nnreal.eq $ real.norm_of_nonneg x.2
 
 end nnreal
@@ -1196,8 +1202,8 @@ end nnreal
 @[simp] lemma norm_norm [semi_normed_group α] (x : α) : ∥∥x∥∥ = ∥x∥ :=
 real.norm_of_nonneg (norm_nonneg _)
 
-@[simp] lemma nnnorm_norm [semi_normed_group α] (a : α) : nnnorm ∥a∥ = nnnorm a :=
-by simp only [nnnorm, norm_norm]
+@[simp] lemma nnnorm_norm [semi_normed_group α] (a : α) : ∥₊∥a∥∥ = ∥₊a∥ :=
+by simpa [real.nnnorm_of_nonneg (norm_nonneg a)]
 
 /-- A restatement of `metric_space.tendsto_at_top` in terms of the norm. -/
 lemma normed_group.tendsto_at_top [nonempty α] [semilattice_sup α] {β : Type*} [semi_normed_group β]
@@ -1223,7 +1229,7 @@ instance : normed_comm_ring ℤ :=
 
 @[norm_cast] lemma int.norm_cast_real (m : ℤ) : ∥(m : ℝ)∥ = ∥m∥ := rfl
 
-lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = nnnorm n :=
+lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = ∥₊n∥ :=
 nnreal.eq $ calc ((n.nat_abs : ℝ≥0) : ℝ)
                = (n.nat_abs : ℤ) : by simp only [int.cast_coe_nat, nnreal.coe_nat_cast]
            ... = abs n           : by simp only [← int.abs_eq_nat_abs, int.cast_abs]
@@ -1270,11 +1276,11 @@ begin
     exact nat.abs_cast n.succ, }
 end
 
-lemma nnnorm_nsmul_le (n : ℕ) (a : α) : nnnorm (n • a) ≤ n * nnnorm a :=
+lemma nnnorm_nsmul_le (n : ℕ) (a : α) : ∥₊n • a∥ ≤ n * ∥₊a∥ :=
 by simpa only [←nnreal.coe_le_coe, nnreal.coe_mul, nnreal.coe_nat_cast]
   using norm_nsmul_le n a
 
-lemma nnnorm_gsmul_le (n : ℤ) (a : α) : nnnorm (n • a) ≤ nnnorm n * nnnorm a :=
+lemma nnnorm_gsmul_le (n : ℤ) (a : α) : ∥₊n • a∥ ≤ ∥₊n∥ * ∥₊a∥ :=
 by simpa only [←nnreal.coe_le_coe, nnreal.coe_mul] using norm_gsmul_le n a
 
 end
@@ -1334,11 +1340,11 @@ end
 lemma dist_smul [semi_normed_space α β] (s : α) (x y : β) : dist (s • x) (s • y) = ∥s∥ * dist x y :=
 by simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub]
 
-lemma nnnorm_smul [semi_normed_space α β] (s : α) (x : β) : nnnorm (s • x) = nnnorm s * nnnorm x :=
+lemma nnnorm_smul [semi_normed_space α β] (s : α) (x : β) : ∥₊s • x∥ = ∥₊s∥ * ∥₊x∥ :=
 nnreal.eq $ norm_smul s x
 
 lemma nndist_smul [semi_normed_space α β] (s : α) (x y : β) :
-  nndist (s • x) (s • y) = nnnorm s * nndist x y :=
+  nndist (s • x) (s • y) = ∥₊s∥ * nndist x y :=
 nnreal.eq $ dist_smul s x y
 
 lemma norm_smul_of_nonneg [semi_normed_space ℝ β] {t : ℝ} (ht : 0 ≤ t) (x : β) :
@@ -1439,8 +1445,8 @@ instance prod.semi_normed_space : semi_normed_space α (E × F) :=
 instance pi.semi_normed_space {E : ι → Type*} [fintype ι] [∀i, semi_normed_group (E i)]
   [∀i, semi_normed_space α (E i)] : semi_normed_space α (Πi, E i) :=
 { norm_smul_le := λ a f, le_of_eq $
-    show (↑(finset.sup finset.univ (λ (b : ι), nnnorm (a • f b))) : ℝ) =
-      nnnorm a * ↑(finset.sup finset.univ (λ (b : ι), nnnorm (f b))),
+    show (↑(finset.sup finset.univ (λ (b : ι), ∥₊a • f b∥)) : ℝ) =
+      ∥₊a∥ * ↑(finset.sup finset.univ (λ (b : ι), ∥₊f b∥)),
     by simp only [(nnreal.coe_mul _ _).symm, nnreal.mul_finset_sup, nnnorm_smul] }
 
 /-- A subspace of a seminormed space is also a normed space, with the restriction of the norm. -/
@@ -1756,13 +1762,13 @@ begin
 end
 
 lemma summable_of_nnnorm_bounded {f : ι → α} (g : ι → ℝ≥0) (hg : summable g)
-  (h : ∀i, nnnorm (f i) ≤ g i) : summable f :=
+  (h : ∀i, ∥₊f i∥ ≤ g i) : summable f :=
 summable_of_norm_bounded (λ i, (g i : ℝ)) (nnreal.summable_coe.2 hg) (λ i, by exact_mod_cast h i)
 
 lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
 summable_of_norm_bounded _ hf (assume i, le_refl _)
 
-lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λa, nnnorm (f a))) : summable f :=
+lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λ a, ∥₊f a∥)) : summable f :=
 summable_of_nnnorm_bounded _ hf (assume i, le_refl _)
 
 end summable

From 369619f6e43e24446ae21c1e3ab160150f7049f6 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Fri, 18 Jun 2021 14:02:32 +0200
Subject: [PATCH 5/9] fix build

---
 src/measure_theory/bochner_integration.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean
index 82dc54e8e84f8..dfee65b3c4733 100644
--- a/src/measure_theory/bochner_integration.lean
+++ b/src/measure_theory/bochner_integration.lean
@@ -1321,7 +1321,7 @@ begin
   apply lintegral_congr_ae,
   filter_upwards [Lp.coe_fn_pos_part f₁, hf.coe_fn_to_L1],
   assume a h₁ h₂,
-  rw [h₁, h₂, ennreal.of_real, nnnorm],
+  rw [h₁, h₂, ennreal.of_real],
   congr' 1,
   apply nnreal.eq,
   simp [real.norm_of_nonneg, le_max_right, real.coe_to_nnreal]
@@ -1334,12 +1334,11 @@ begin
   apply lintegral_congr_ae,
   filter_upwards [Lp.coe_fn_neg_part f₁, hf.coe_fn_to_L1],
   assume a h₁ h₂,
-  rw [h₁, h₂, ennreal.of_real, nnnorm],
+  rw [h₁, h₂, ennreal.of_real],
   congr' 1,
   apply nnreal.eq,
   simp only [real.norm_of_nonneg, min_le_right, neg_nonneg, real.coe_to_nnreal', subtype.coe_mk],
-  rw ← max_neg_neg,
-  simp,
+  rw [← max_neg_neg, coe_nnnorm, neg_zero, real.norm_of_nonneg (le_max_right (-f a) 0)]
 end,
 begin
   rw [eq₁, eq₂, integral, dif_pos],

From b3aab3083d46a5ae257e5f011c99be9c6f570241 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Fri, 18 Jun 2021 17:02:35 +0200
Subject: [PATCH 6/9] lint

---
 src/analysis/normed_space/basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 5b3f862a36864..52267259b9f87 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -366,6 +366,7 @@ export has_nnnorm (nnnorm)
 
 notation `∥₊`:1024 e:1 `∥`:1 := nnnorm e
 
+@[priority 100] -- see Note [lower instance priority]
 instance semi_normed_group.to_has_nnnorm : has_nnnorm α := ⟨λ a, ⟨norm a, norm_nonneg a⟩⟩
 
 @[simp, norm_cast] lemma coe_nnnorm (a : α) : (∥₊a∥ : ℝ) = norm a := rfl

From b9a93c54ab219b06fce61fa018c7428155cefd3d Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Sat, 19 Jun 2021 10:30:53 +0200
Subject: [PATCH 7/9] lint

---
 src/topology/metric_space/basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
index 92bf8aa294802..25e6c06ec8c9a 100644
--- a/src/topology/metric_space/basic.lean
+++ b/src/topology/metric_space/basic.lean
@@ -198,6 +198,7 @@ export has_nndist (nndist)
 
 
 /-- Distance as a nonnegative real number. -/
+@[priority 100] -- see Note [lower instance priority]
 instance pseudo_metric_space.to_has_nndist : has_nndist α := ⟨λ a b, ⟨dist a b, dist_nonneg⟩⟩
 
 /--Express `nndist` in terms of `edist`-/

From 40f86c7588e62e9cbe2f2c66c5f39f5e228ff31a Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Mon, 21 Jun 2021 13:07:20 +0200
Subject: [PATCH 8/9] better notation

---
 src/analysis/normed_space/basic.lean | 96 ++++++++++++++--------------
 1 file changed, 48 insertions(+), 48 deletions(-)

diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 52267259b9f87..f886b8c2c6c40 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -364,37 +364,37 @@ class has_nnnorm (α : Type*) := (nnnorm : α → ℝ≥0)
 
 export has_nnnorm (nnnorm)
 
-notation `∥₊`:1024 e:1 `∥`:1 := nnnorm e
+notation `∥`e`∥₊` := nnnorm e
 
 @[priority 100] -- see Note [lower instance priority]
 instance semi_normed_group.to_has_nnnorm : has_nnnorm α := ⟨λ a, ⟨norm a, norm_nonneg a⟩⟩
 
-@[simp, norm_cast] lemma coe_nnnorm (a : α) : (∥₊a∥ : ℝ) = norm a := rfl
+@[simp, norm_cast] lemma coe_nnnorm (a : α) : (∥a∥₊ : ℝ) = norm a := rfl
 
-lemma nndist_eq_nnnorm (a b : α) : nndist a b = ∥₊a - b∥ := nnreal.eq $ dist_eq_norm _ _
+lemma nndist_eq_nnnorm (a b : α) : nndist a b = ∥a - b∥₊ := nnreal.eq $ dist_eq_norm _ _
 
-@[simp] lemma nnnorm_zero : ∥₊(0 : α)∥ = 0 :=
+@[simp] lemma nnnorm_zero : ∥(0 : α)∥₊ = 0 :=
 nnreal.eq norm_zero
 
-lemma nnnorm_add_le (g h : α) : ∥₊g + h∥ ≤ ∥₊g∥ + ∥₊h∥ :=
+lemma nnnorm_add_le (g h : α) : ∥g + h∥₊ ≤ ∥g∥₊ + ∥h∥₊ :=
 nnreal.coe_le_coe.2 $ norm_add_le g h
 
-@[simp] lemma nnnorm_neg (g : α) : ∥₊-g∥ = ∥₊g∥ :=
+@[simp] lemma nnnorm_neg (g : α) : ∥-g∥₊ = ∥g∥₊ :=
 nnreal.eq $ norm_neg g
 
-lemma nndist_nnnorm_nnnorm_le (g h : α) : nndist ∥₊g∥ ∥₊h∥ ≤ ∥₊g - h∥ :=
+lemma nndist_nnnorm_nnnorm_le (g h : α) : nndist ∥g∥₊ ∥h∥₊ ≤ ∥g - h∥₊ :=
 nnreal.coe_le_coe.2 $ dist_norm_norm_le g h
 
-lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (∥₊x∥ : ℝ≥0∞) :=
+lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (∥x∥₊ : ℝ≥0∞) :=
 ennreal.of_real_eq_coe_nnreal _
 
-lemma edist_eq_coe_nnnorm_sub (x y : β) : edist x y = (∥₊x - y∥ : ℝ≥0∞) :=
+lemma edist_eq_coe_nnnorm_sub (x y : β) : edist x y = (∥x - y∥₊ : ℝ≥0∞) :=
 by rw [edist_dist, dist_eq_norm, of_real_norm_eq_coe_nnnorm]
 
-lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (∥₊x∥ : ℝ≥0∞) :=
+lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (∥x∥₊ : ℝ≥0∞) :=
 by rw [edist_eq_coe_nnnorm_sub, _root_.sub_zero]
 
-lemma mem_emetric_ball_0_iff {x : β} {r : ℝ≥0∞} : x ∈ emetric.ball (0 : β) r ↔ ↑∥₊x∥ < r :=
+lemma mem_emetric_ball_0_iff {x : β} {r : ℝ≥0∞} : x ∈ emetric.ball (0 : β) r ↔ ↑∥x∥₊ < r :=
 by rw [emetric.mem_ball, edist_eq_coe_nnnorm]
 
 lemma nndist_add_add_le (g₁ g₂ h₁ h₂ : α) :
@@ -406,7 +406,7 @@ lemma edist_add_add_le (g₁ g₂ h₁ h₂ : α) :
 by { simp only [edist_nndist], norm_cast, apply nndist_add_add_le }
 
 lemma nnnorm_sum_le {β} : ∀(s : finset β) (f : β → α),
-  ∥₊∑ a in s, f a∥ ≤ ∑ a in s, ∥₊f a∥ :=
+  ∥∑ a in s, f a∥₊ ≤ ∑ a in s, ∥f a∥₊ :=
 finset.le_sum_of_subadditive nnnorm nnnorm_zero nnnorm_add_le
 
 end nnnorm
@@ -492,7 +492,7 @@ instance prod.semi_normed_group : semi_normed_group (α × β) :=
 
 lemma prod.semi_norm_def (x : α × β) : ∥x∥ = (max ∥x.1∥ ∥x.2∥) := rfl
 
-lemma prod.nnsemi_norm_def (x : α × β) : ∥₊x∥ = max ∥₊x.1∥ ∥₊x.2∥ :=
+lemma prod.nnsemi_norm_def (x : α × β) : ∥x∥₊ = max (∥x.1∥₊) (∥x.2∥₊) :=
 by { have := x.semi_norm_def, simp only [← coe_nnnorm] at this, exact_mod_cast this }
 
 lemma semi_norm_fst_le (x : α × β) : ∥x.1∥ ≤ ∥x∥ :=
@@ -509,10 +509,10 @@ max_le_iff
 using the sup norm. -/
 instance pi.semi_normed_group {π : ι → Type*} [fintype ι] [∀i, semi_normed_group (π i)] :
   semi_normed_group (Πi, π i) :=
-{ norm := λf, ((finset.sup finset.univ (λ b, ∥₊f b∥) : ℝ≥0) : ℝ),
+{ norm := λf, ((finset.sup finset.univ (λ b, ∥f b∥₊) : ℝ≥0) : ℝ),
   dist_eq := assume x y,
     congr_arg (coe : ℝ≥0 → ℝ) $ congr_arg (finset.sup finset.univ) $ funext $ assume a,
-    show nndist (x a) (y a) = ∥₊x a - y a∥, from nndist_eq_nnnorm _ _ }
+    show nndist (x a) (y a) = ∥x a - y a∥₊, from nndist_eq_nnnorm _ _ }
 
 /-- The seminorm of an element in a product space is `≤ r` if and only if the norm of each
 component is. -/
@@ -534,7 +534,7 @@ lemma semi_norm_le_pi_norm {π : ι → Type*} [fintype ι] [∀i, semi_normed_g
 by simpa only [← dist_zero_right] using dist_pi_const a 0
 
 @[simp] lemma pi_nnsemi_norm_const [nonempty ι] [fintype ι] (a : α) :
-  ∥₊(λ i : ι, a)∥ = ∥₊a∥ :=
+  ∥(λ i : ι, a)∥₊ = ∥a∥₊ :=
 nnreal.eq $ pi_semi_norm_const a
 
 lemma tendsto_iff_norm_tendsto_zero {f : ι → β} {a : filter ι} {b : β} :
@@ -584,7 +584,7 @@ lemma continuous_norm : continuous (λg:α, ∥g∥) :=
 by simpa using continuous_id.dist (continuous_const : continuous (λ g, (0:α)))
 
 @[continuity]
-lemma continuous_nnnorm : continuous (λ (a : α), ∥₊a∥) :=
+lemma continuous_nnnorm : continuous (λ (a : α), ∥a∥₊) :=
 continuous_subtype_mk _ continuous_norm
 
 lemma lipschitz_with_one_norm : lipschitz_with 1 (norm : α → ℝ) :=
@@ -593,7 +593,7 @@ by simpa only [dist_zero_left] using lipschitz_with.dist_right (0 : α)
 lemma uniform_continuous_norm : uniform_continuous (norm : α → ℝ) :=
 lipschitz_with_one_norm.uniform_continuous
 
-lemma uniform_continuous_nnnorm : uniform_continuous (λ (a : α), ∥₊a∥) :=
+lemma uniform_continuous_nnnorm : uniform_continuous (λ (a : α), ∥a∥₊) :=
 uniform_continuous_subtype_mk uniform_continuous_norm _
 
 section
@@ -604,7 +604,7 @@ lemma filter.tendsto.norm {a : α} (h : tendsto f l (𝓝 a)) : tendsto (λ x, 
 tendsto_norm.comp h
 
 lemma filter.tendsto.nnnorm (h : tendsto f l (𝓝 a)) :
-  tendsto (λ x, ∥₊f x∥) l (𝓝 (∥₊a∥)) :=
+  tendsto (λ x, ∥f x∥₊) l (𝓝 (∥a∥₊)) :=
 tendsto.comp continuous_nnnorm.continuous_at h
 
 end
@@ -615,25 +615,25 @@ variables [topological_space γ] {f : γ → α} {s : set γ} {a : γ} {b : α}
 
 lemma continuous.norm (h : continuous f) : continuous (λ x, ∥f x∥) := continuous_norm.comp h
 
-lemma continuous.nnnorm (h : continuous f) : continuous (λ x, ∥₊f x∥) :=
+lemma continuous.nnnorm (h : continuous f) : continuous (λ x, ∥f x∥₊) :=
 continuous_nnnorm.comp h
 
 lemma continuous_at.norm (h : continuous_at f a) : continuous_at (λ x, ∥f x∥) a := h.norm
 
-lemma continuous_at.nnnorm (h : continuous_at f a) : continuous_at (λ x, ∥₊f x∥) a := h.nnnorm
+lemma continuous_at.nnnorm (h : continuous_at f a) : continuous_at (λ x, ∥f x∥₊) a := h.nnnorm
 
 lemma continuous_within_at.norm (h : continuous_within_at f s a) :
   continuous_within_at (λ x, ∥f x∥) s a :=
 h.norm
 
 lemma continuous_within_at.nnnorm (h : continuous_within_at f s a) :
-  continuous_within_at (λ x, ∥₊f x∥) s a :=
+  continuous_within_at (λ x, ∥f x∥₊) s a :=
 h.nnnorm
 
 lemma continuous_on.norm (h : continuous_on f s) : continuous_on (λ x, ∥f x∥) s :=
 λ x hx, (h x hx).norm
 
-lemma continuous_on.nnnorm (h : continuous_on f s) : continuous_on (λ x, ∥₊f x∥) s :=
+lemma continuous_on.nnnorm (h : continuous_on f s) : continuous_on (λ x, ∥f x∥₊) s :=
 λ x hx, (h x hx).nnnorm
 
 end
@@ -761,7 +761,7 @@ begin
   rwa dist_eq_norm
 end
 
-@[simp] lemma nnnorm_eq_zero {a : α} : ∥₊a∥ = 0 ↔ a = 0 :=
+@[simp] lemma nnnorm_eq_zero {a : α} : ∥a∥₊ = 0 ↔ a = 0 :=
 by simp only [nnreal.eq_iff.symm, nnreal.coe_zero, coe_nnnorm, norm_eq_zero]
 
 /-- A subgroup of a normed group is also a normed group, with the restriction of the norm. -/
@@ -781,7 +781,7 @@ instance prod.normed_group : normed_group (α × β) := { ..prod.semi_normed_gro
 
 lemma prod.norm_def (x : α × β) : ∥x∥ = (max ∥x.1∥ ∥x.2∥) := rfl
 
-lemma prod.nnnorm_def (x : α × β) : ∥₊x∥ = max ∥₊x.1∥ ∥₊x.2∥ :=
+lemma prod.nnnorm_def (x : α × β) : ∥x∥₊ = max (∥x.1∥₊) (∥x.2∥₊) :=
 by { have := x.norm_def, simp only [← coe_nnnorm] at this, exact_mod_cast this }
 
 lemma norm_fst_le (x : α × β) : ∥x.1∥ ≤ ∥x∥ :=
@@ -818,7 +818,7 @@ lemma norm_le_pi_norm {π : ι → Type*} [fintype ι] [∀i, normed_group (π i
 by simpa only [← dist_zero_right] using dist_pi_const a 0
 
 @[simp] lemma pi_nnnorm_const [nonempty ι] [fintype ι] (a : α) :
-  ∥₊(λ i : ι, a)∥ = ∥₊a∥ :=
+  ∥(λ i : ι, a)∥₊ = ∥a∥₊ :=
 nnreal.eq $ pi_norm_const a
 
 lemma tendsto_norm_nhds_within_zero : tendsto (norm : α → ℝ) (𝓝[{0}ᶜ] 0) (𝓝[set.Ioi 0] 0) :=
@@ -874,7 +874,7 @@ export norm_one_class (norm_one)
 
 attribute [simp] norm_one
 
-@[simp] lemma nnnorm_one [semi_normed_group α] [has_one α] [norm_one_class α] : ∥₊(1:α)∥ = 1 :=
+@[simp] lemma nnnorm_one [semi_normed_group α] [has_one α] [norm_one_class α] : ∥(1 : α)∥₊ = 1 :=
 nnreal.eq norm_one
 
 @[priority 100] -- see Note [lower instance priority]
@@ -1054,7 +1054,7 @@ instance to_norm_one_class : norm_one_class α :=
 ⟨mul_left_cancel' (mt norm_eq_zero.1 (@one_ne_zero α _ _)) $
   by rw [← norm_mul, mul_one, mul_one]⟩
 
-@[simp] lemma nnnorm_mul (a b : α) : ∥₊a * b∥ = ∥₊a∥ * ∥₊b∥ :=
+@[simp] lemma nnnorm_mul (a b : α) : ∥a * b∥₊ = ∥a∥₊ * ∥b∥₊ :=
 nnreal.eq $ norm_mul a b
 
 /-- `norm` as a `monoid_hom`. -/
@@ -1067,7 +1067,7 @@ nnreal.eq $ norm_mul a b
 @[simp] lemma norm_pow (a : α) : ∀ (n : ℕ), ∥a ^ n∥ = ∥a∥ ^ n :=
 (norm_hom.to_monoid_hom : α →* ℝ).map_pow a
 
-@[simp] lemma nnnorm_pow (a : α) (n : ℕ) : ∥₊a ^ n∥ = ∥₊a∥ ^ n :=
+@[simp] lemma nnnorm_pow (a : α) (n : ℕ) : ∥a ^ n∥₊ = ∥a∥₊ ^ n :=
 (nnnorm_hom.to_monoid_hom : α →* ℝ≥0).map_pow a n
 
 @[simp] lemma norm_prod (s : finset β) (f : β → α) :
@@ -1075,25 +1075,25 @@ nnreal.eq $ norm_mul a b
 (norm_hom.to_monoid_hom : α →* ℝ).map_prod f s
 
 @[simp] lemma nnnorm_prod (s : finset β) (f : β → α) :
-  ∥₊∏ b in s, f b∥ = ∏ b in s, ∥₊f b∥ :=
+  ∥∏ b in s, f b∥₊ = ∏ b in s, ∥f b∥₊ :=
 (nnnorm_hom.to_monoid_hom : α →* ℝ≥0).map_prod f s
 
 @[simp] lemma norm_div (a b : α) : ∥a / b∥ = ∥a∥ / ∥b∥ :=
 (norm_hom : monoid_with_zero_hom α ℝ).map_div a b
 
-@[simp] lemma nnnorm_div (a b : α) : ∥₊a / b∥ = ∥₊a∥ / ∥₊b∥ :=
+@[simp] lemma nnnorm_div (a b : α) : ∥a / b∥₊ = ∥a∥₊ / ∥b∥₊ :=
 (nnnorm_hom : monoid_with_zero_hom α ℝ≥0).map_div a b
 
 @[simp] lemma norm_inv (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ :=
 (norm_hom : monoid_with_zero_hom α ℝ).map_inv' a
 
-@[simp] lemma nnnorm_inv (a : α) : ∥₊a⁻¹∥ = ∥₊a∥⁻¹ :=
+@[simp] lemma nnnorm_inv (a : α) : ∥a⁻¹∥₊ = ∥a∥₊⁻¹ :=
 nnreal.eq $ by simp
 
 @[simp] lemma norm_fpow : ∀ (a : α) (n : ℤ), ∥a^n∥ = ∥a∥^n :=
 (norm_hom : monoid_with_zero_hom α ℝ).map_fpow
 
-@[simp] lemma nnnorm_fpow : ∀ (a : α) (n : ℤ), ∥₊a ^ n∥ = ∥₊a∥ ^ n :=
+@[simp] lemma nnnorm_fpow : ∀ (a : α) (n : ℤ), ∥a ^ n∥₊ = ∥a∥₊ ^ n :=
 (nnnorm_hom : monoid_with_zero_hom α ℝ≥0).map_fpow
 
 @[priority 100] -- see Note [lower instance priority]
@@ -1174,16 +1174,16 @@ abs_of_nonneg hx
 
 @[simp] lemma norm_coe_nat (n : ℕ) : ∥(n : ℝ)∥ = n := abs_of_nonneg n.cast_nonneg
 
-@[simp] lemma nnnorm_coe_nat (n : ℕ) : ∥₊(n : ℝ)∥ = n := nnreal.eq $ by simp
+@[simp] lemma nnnorm_coe_nat (n : ℕ) : ∥(n : ℝ)∥₊ = n := nnreal.eq $ by simp
 
 @[simp] lemma norm_two : ∥(2 : ℝ)∥ = 2 := abs_of_pos (@zero_lt_two ℝ _ _)
 
-@[simp] lemma nnnorm_two : ∥₊(2 : ℝ)∥ = 2 := nnreal.eq $ by simp
+@[simp] lemma nnnorm_two : ∥(2 : ℝ)∥₊ = 2 := nnreal.eq $ by simp
 
-lemma nnnorm_of_nonneg {x : ℝ} (hx : 0 ≤ x) : ∥₊x∥ = ⟨x, hx⟩ :=
+lemma nnnorm_of_nonneg {x : ℝ} (hx : 0 ≤ x) : ∥x∥₊ = ⟨x, hx⟩ :=
 nnreal.eq $ norm_of_nonneg hx
 
-lemma ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) : (∥₊x∥ : ℝ≥0∞) = ennreal.of_real x :=
+lemma ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) : (∥x∥₊ : ℝ≥0∞) = ennreal.of_real x :=
 by { rw [← of_real_norm_eq_coe_nnnorm, norm_of_nonneg hx] }
 
 end real
@@ -1195,7 +1195,7 @@ open_locale nnreal
 @[simp] lemma norm_eq (x : ℝ≥0) : ∥(x : ℝ)∥ = x :=
 by rw [real.norm_eq_abs, x.abs_eq]
 
-@[simp] lemma nnnorm_eq (x : ℝ≥0) : ∥₊(x : ℝ)∥ = x :=
+@[simp] lemma nnnorm_eq (x : ℝ≥0) : ∥(x : ℝ)∥₊ = x :=
 nnreal.eq $ real.norm_of_nonneg x.2
 
 end nnreal
@@ -1203,7 +1203,7 @@ end nnreal
 @[simp] lemma norm_norm [semi_normed_group α] (x : α) : ∥∥x∥∥ = ∥x∥ :=
 real.norm_of_nonneg (norm_nonneg _)
 
-@[simp] lemma nnnorm_norm [semi_normed_group α] (a : α) : ∥₊∥a∥∥ = ∥₊a∥ :=
+@[simp] lemma nnnorm_norm [semi_normed_group α] (a : α) : ∥∥a∥∥₊ = ∥a∥₊ :=
 by simpa [real.nnnorm_of_nonneg (norm_nonneg a)]
 
 /-- A restatement of `metric_space.tendsto_at_top` in terms of the norm. -/
@@ -1230,7 +1230,7 @@ instance : normed_comm_ring ℤ :=
 
 @[norm_cast] lemma int.norm_cast_real (m : ℤ) : ∥(m : ℝ)∥ = ∥m∥ := rfl
 
-lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = ∥₊n∥ :=
+lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = ∥n∥₊ :=
 nnreal.eq $ calc ((n.nat_abs : ℝ≥0) : ℝ)
                = (n.nat_abs : ℤ) : by simp only [int.cast_coe_nat, nnreal.coe_nat_cast]
            ... = abs n           : by simp only [← int.abs_eq_nat_abs, int.cast_abs]
@@ -1277,11 +1277,11 @@ begin
     exact nat.abs_cast n.succ, }
 end
 
-lemma nnnorm_nsmul_le (n : ℕ) (a : α) : ∥₊n • a∥ ≤ n * ∥₊a∥ :=
+lemma nnnorm_nsmul_le (n : ℕ) (a : α) : ∥n • a∥₊ ≤ n * ∥a∥₊ :=
 by simpa only [←nnreal.coe_le_coe, nnreal.coe_mul, nnreal.coe_nat_cast]
   using norm_nsmul_le n a
 
-lemma nnnorm_gsmul_le (n : ℤ) (a : α) : ∥₊n • a∥ ≤ ∥₊n∥ * ∥₊a∥ :=
+lemma nnnorm_gsmul_le (n : ℤ) (a : α) : ∥n • a∥₊ ≤ ∥n∥₊ * ∥a∥₊ :=
 by simpa only [←nnreal.coe_le_coe, nnreal.coe_mul] using norm_gsmul_le n a
 
 end
@@ -1341,11 +1341,11 @@ end
 lemma dist_smul [semi_normed_space α β] (s : α) (x y : β) : dist (s • x) (s • y) = ∥s∥ * dist x y :=
 by simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub]
 
-lemma nnnorm_smul [semi_normed_space α β] (s : α) (x : β) : ∥₊s • x∥ = ∥₊s∥ * ∥₊x∥ :=
+lemma nnnorm_smul [semi_normed_space α β] (s : α) (x : β) : ∥s • x∥₊ = ∥s∥₊ * ∥x∥₊ :=
 nnreal.eq $ norm_smul s x
 
 lemma nndist_smul [semi_normed_space α β] (s : α) (x y : β) :
-  nndist (s • x) (s • y) = ∥₊s∥ * nndist x y :=
+  nndist (s • x) (s • y) = ∥s∥₊ * nndist x y :=
 nnreal.eq $ dist_smul s x y
 
 lemma norm_smul_of_nonneg [semi_normed_space ℝ β] {t : ℝ} (ht : 0 ≤ t) (x : β) :
@@ -1446,8 +1446,8 @@ instance prod.semi_normed_space : semi_normed_space α (E × F) :=
 instance pi.semi_normed_space {E : ι → Type*} [fintype ι] [∀i, semi_normed_group (E i)]
   [∀i, semi_normed_space α (E i)] : semi_normed_space α (Πi, E i) :=
 { norm_smul_le := λ a f, le_of_eq $
-    show (↑(finset.sup finset.univ (λ (b : ι), ∥₊a • f b∥)) : ℝ) =
-      ∥₊a∥ * ↑(finset.sup finset.univ (λ (b : ι), ∥₊f b∥)),
+    show (↑(finset.sup finset.univ (λ (b : ι), ∥a • f b∥₊)) : ℝ) =
+      ∥a∥₊ * ↑(finset.sup finset.univ (λ (b : ι), ∥f b∥₊)),
     by simp only [(nnreal.coe_mul _ _).symm, nnreal.mul_finset_sup, nnnorm_smul] }
 
 /-- A subspace of a seminormed space is also a normed space, with the restriction of the norm. -/
@@ -1763,13 +1763,13 @@ begin
 end
 
 lemma summable_of_nnnorm_bounded {f : ι → α} (g : ι → ℝ≥0) (hg : summable g)
-  (h : ∀i, ∥₊f i∥ ≤ g i) : summable f :=
+  (h : ∀i, ∥f i∥₊ ≤ g i) : summable f :=
 summable_of_norm_bounded (λ i, (g i : ℝ)) (nnreal.summable_coe.2 hg) (λ i, by exact_mod_cast h i)
 
 lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
 summable_of_norm_bounded _ hf (assume i, le_refl _)
 
-lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λ a, ∥₊f a∥)) : summable f :=
+lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λ a, ∥f a∥₊)) : summable f :=
 summable_of_nnnorm_bounded _ hf (assume i, le_refl _)
 
 end summable

From 9b8953475a857b9c20d1a1479e8ccc8c0c7bd9ad Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Mon, 21 Jun 2021 14:57:46 +0200
Subject: [PATCH 9/9] this was misleading

---
 src/analysis/normed_space/basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index f886b8c2c6c40..ef5973e936922 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -29,7 +29,7 @@ class has_norm (α : Type*) := (norm : α → ℝ)
 
 export has_norm (norm)
 
-notation `∥`:1024 e:1 `∥`:1 := norm e
+notation `∥` e `∥` := norm e
 
 /-- A seminormed group is an additive group endowed with a norm for which `dist x y = ∥x - y∥`
 defines a pseudometric space structure. -/