feat(analysis/normed_space/operator_norm): continuity of linear forms…

…; swap directions of `nnreal.coe_*` (#1655)

* feat(analysis/normed_space/operator_norm): continuity of linear forms

* use lift, change nnreal.coe_le direction

src/analysis/normed_space/operator_norm.lean

@@ -9,7 +9,7 @@ Define the operator norm on the space of continuous linear maps between normed s
 its basic properties. In particular, show that this space is itself a normed space.
 -/
 
-import topology.metric_space.lipschitz
+import topology.metric_space.lipschitz analysis.normed_space.riesz_lemma
 import analysis.asymptotics
 noncomputable theory
 open_locale classical
@@ -27,11 +27,15 @@ lemma exists_pos_bound_of_bound {f : E → F} (M : ℝ) (h : ∀x, ∥f x∥ ≤
   ∥f x∥ ≤ M * ∥x∥ : h x
   ... ≤ max M 1 * ∥x∥ : mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) ⟩
 
-variables [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [normed_space 𝕜 G]
-(c : 𝕜) (f g : E →L[𝕜] F) (h : F →L[𝕜] G) (x y z : E)
-include 𝕜
+section normed_field
+/- Most statements in this file require the field to be non-discrete, as this is necessary
+to deduce an inequality ∥f x∥ ≤ C ∥x∥ from the continuity of f. However, the other direction always
+holds. In this section, we just assume that 𝕜 is a normed field. In the remainder of the file,
+it will be non-discrete. -/
+
+variables [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E →ₗ[𝕜] F)
 
-lemma linear_map.continuous_of_bound (f : E →ₗ[𝕜] F) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
+lemma linear_map.continuous_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   continuous f :=
 begin
   have : ∀ (x y : E), dist (f x) (f y) ≤ C * dist x y := λx y, calc
@@ -43,24 +47,84 @@ begin
 end
 
 /-- Construct a continuous linear map from a linear map and a bound on this linear map. -/
-def linear_map.with_bound (f : E →ₗ[𝕜] F) (h : ∃C : ℝ, ∀x, ∥f x∥ ≤ C * ∥x∥) : E →L[𝕜] F :=
+def linear_map.with_bound (h : ∃C : ℝ, ∀x, ∥f x∥ ≤ C * ∥x∥) : E →L[𝕜] F :=
 ⟨f, let ⟨C, hC⟩ := h in linear_map.continuous_of_bound f C hC⟩
 
-@[simp, elim_cast] lemma linear_map_with_bound_coe (f : E →ₗ[𝕜] F) (h : ∃C : ℝ, ∀x, ∥f x∥ ≤ C * ∥x∥) :
+@[simp, elim_cast] lemma linear_map_with_bound_coe (h : ∃C : ℝ, ∀x, ∥f x∥ ≤ C * ∥x∥) :
   ((f.with_bound h) : E →ₗ[𝕜] F) = f := rfl
 
-@[simp] lemma linear_map_with_bound_apply (f : E →ₗ[𝕜] F) (h : ∃C : ℝ, ∀x, ∥f x∥ ≤ C * ∥x∥) (x : E) :
+@[simp] lemma linear_map_with_bound_apply (h : ∃C : ℝ, ∀x, ∥f x∥ ≤ C * ∥x∥) (x : E) :
   f.with_bound h x = f x := rfl
 
-namespace continuous_linear_map
+lemma linear_map.continuous_iff_is_closed_ker {f : E →ₗ[𝕜] 𝕜} :
+  continuous f ↔ is_closed (f.ker : set E) :=
+begin
+  -- the continuity of f obviously implies that its kernel is closed
+  refine ⟨λh, (continuous_iff_is_closed.1 h) {0} (t1_space.t1 0), λh, _⟩,
+  -- for the other direction, we assume that the kernel is closed
+  by_cases hf : ∀x, x ∈ f.ker,
+  { -- if f = 0, its continuity is obvious
+    have : (f : E → 𝕜) = (λx, 0), by { ext x, simpa using hf x },
+    rw this,
+    exact continuous_const },
+  { /- if f is not zero, we use an element x₀ ∉ ker f such taht ∥x₀∥ ≤ 2 ∥x₀ - y∥ for all y ∈ ker f,
+    given by Riesz's lemma, and prove that 2 ∥f x₀∥ / ∥x₀∥ gives a bound on the operator norm of f.
+    For this, start from an arbitrary x and note that y = x₀ - (f x₀ / f x) x belongs to the kernel
+    of f. Applying the above inequality to x₀ and y readily gives the conclusion. -/
+    push_neg at hf,
+    let r : ℝ := (2 : ℝ)⁻¹,
+    have : 0 ≤ r, by norm_num [r],
+    have : r < 1, by norm_num [r],
+    obtain ⟨x₀, x₀ker, h₀⟩ : ∃ (x₀ : E), x₀ ∉ f.ker ∧ ∀ y ∈ linear_map.ker f, r * ∥x₀∥ ≤ ∥x₀ - y∥,
+      from riesz_lemma h hf this,
+    have : x₀ ≠ 0,
+    { assume h,
+      have : x₀ ∈ f.ker, by { rw h, exact (linear_map.ker f).zero },
+      exact x₀ker this },
+    have rx₀_ne_zero : r * ∥x₀∥ ≠ 0, by { simp [norm_eq_zero, this], norm_num },
+    have : ∀x, ∥f x∥ ≤ (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥,
+    { assume x,
+      by_cases hx : f x = 0,
+      { rw [hx, norm_zero],
+        apply_rules [mul_nonneg', norm_nonneg, inv_nonneg.2, norm_nonneg] },
+      { let y := x₀ - (f x₀ * (f x)⁻¹ ) • x,
+        have fy_zero : f y = 0, by calc
+          f y = f x₀ - (f x₀ * (f x)⁻¹ ) * f x :
+            by { dsimp [y], rw [f.map_add, f.map_neg, f.map_smul], refl }
+          ... = 0 :
+            by { rw [mul_assoc, inv_mul_cancel hx, mul_one, sub_eq_zero_of_eq], refl },
+        have A : r * ∥x₀∥ ≤ ∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥, from calc
+          r * ∥x₀∥ ≤ ∥x₀ - y∥ : h₀ _ (linear_map.mem_ker.2 fy_zero)
+          ... = ∥(f x₀ * (f x)⁻¹ ) • x∥ : by { dsimp [y], congr, abel }
+          ... = ∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥ :
+            by rw [norm_smul, normed_field.norm_mul, normed_field.norm_inv],
+        calc
+          ∥f x∥ = (r * ∥x₀∥)⁻¹ * (r * ∥x₀∥) * ∥f x∥ : by rwa [inv_mul_cancel, one_mul]
+          ... ≤ (r * ∥x₀∥)⁻¹ * (∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥) * ∥f x∥ : begin
+            apply mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left A _) (norm_nonneg _),
+            exact inv_nonneg.2 (mul_nonneg' (by norm_num) (norm_nonneg _))
+          end
+          ... = (∥f x∥ ⁻¹ * ∥f x∥) * (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ : by ring
+          ... = (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ :
+            by { rw [inv_mul_cancel, one_mul], simp [norm_eq_zero, hx] } } },
+    exact linear_map.continuous_of_bound f _ this }
+end
+
+end normed_field
+
+variables [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [normed_space 𝕜 G]
+(c : 𝕜) (f g : E →L[𝕜] F) (h : F →L[𝕜] G) (x y z : E)
+include 𝕜
+
 
 /-- A continuous linear map between normed spaces is bounded when the field is nondiscrete.
 The continuity ensures boundedness on a ball of some radius δ. The nondiscreteness is then
 used to rescale any element into an element of norm in [δ/C, δ], whose image has a controlled norm.
 The norm control for the original element follows by rescaling. -/
-theorem bound : ∃ C, 0 < C ∧ (∀ x : E, ∥f x∥ ≤ C * ∥x∥) :=
+lemma linear_map.bound_of_continuous (f : E →ₗ[𝕜] F) (hf : continuous f) :
+  ∃ C, 0 < C ∧ (∀ x : E, ∥f x∥ ≤ C * ∥x∥) :=
 begin
-  have : continuous_at f 0 := continuous_iff_continuous_at.1 f.2 _,
+  have : continuous_at f 0 := continuous_iff_continuous_at.1 hf _,
   rcases metric.tendsto_nhds_nhds.1 this 1 zero_lt_one with ⟨ε, ε_pos, hε⟩,
   let δ := ε/2,
   have δ_pos : δ > 0 := half_pos ε_pos,
@@ -74,17 +138,22 @@ begin
   rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
   refine ⟨δ⁻¹ * ∥c∥, mul_pos (inv_pos δ_pos) (lt_trans zero_lt_one hc), (λx, _)⟩,
   by_cases h : x = 0,
-  { simp only [h, norm_zero, mul_zero, continuous_linear_map.map_zero], },
+  { simp only [h, norm_zero, mul_zero, linear_map.map_zero] },
   { rcases rescale_to_shell hc δ_pos h with ⟨d, hd, dxle, ledx, dinv⟩,
     calc ∥f x∥
       = ∥f ((d⁻¹ * d) • x)∥ : by rwa [inv_mul_cancel, one_smul]
       ... = ∥d∥⁻¹ * ∥f (d • x)∥ :
-        by rw [mul_smul, map_smul, norm_smul, normed_field.norm_inv]
+        by rw [mul_smul, linear_map.map_smul, norm_smul, normed_field.norm_inv]
       ... ≤ ∥d∥⁻¹ * 1 :
         mul_le_mul_of_nonneg_left (H dxle) (by { rw ← normed_field.norm_inv, exact norm_nonneg _ })
       ... ≤ δ⁻¹ * ∥c∥ * ∥x∥ : by { rw mul_one, exact dinv } }
 end
 
+namespace continuous_linear_map
+
+theorem bound : ∃ C, 0 < C ∧ (∀ x : E, ∥f x∥ ≤ C * ∥x∥) :=
+f.to_linear_map.bound_of_continuous f.2
+
 section
 open asymptotics filter
 
@@ -230,6 +299,60 @@ theorem lipschitz : lipschitz_with ∥f∥ f :=
 ⟨op_norm_nonneg _, λ x y,
   by { rw [dist_eq_norm, dist_eq_norm, ←map_sub], apply le_op_norm }⟩
 
+/-- A continuous linear map is automatically uniformly continuous. -/
+theorem uniform_continuous : uniform_continuous f :=
+f.lipschitz.to_uniform_continuous
+
+/-- A continuous linear map is a uniform embedding if it expands the norm by a constant factor. -/
+theorem uniform_embedding_of_bound (C : ℝ) (hC : ∀x, ∥x∥ ≤ C * ∥f x∥) :
+  uniform_embedding f :=
+begin
+  have Cpos : 0 < max C 1 := lt_of_lt_of_le zero_lt_one (le_max_right _ _),
+  refine uniform_embedding_iff'.2 ⟨metric.uniform_continuous_iff.1 (uniform_continuous _),
+                                    λδ δpos, ⟨δ / (max C 1), div_pos δpos Cpos, λx y hxy, _⟩⟩,
+  calc dist x y = ∥x - y∥ : by rw dist_eq_norm
+  ... ≤ C * ∥f (x - y)∥ : hC _
+  ... = C * dist (f x) (f y) : by rw [f.map_sub, dist_eq_norm]
+  ... ≤ max C 1 * dist (f x) (f y) :
+    mul_le_mul_of_nonneg_right (le_max_left _ _) dist_nonneg
+  ... < max C 1 * (δ / max C 1) : mul_lt_mul_of_pos_left hxy Cpos
+  ... = δ : by { rw mul_comm, exact div_mul_cancel _ (ne_of_lt Cpos).symm }
+end
+
+/-- If a continuous linear map is a uniform embedding, then it expands the norm by a positive
+factor.-/
+theorem bound_of_uniform_embedding (hf : uniform_embedding f) :
+  ∃ C : ℝ, 0 < C ∧ ∀x, ∥x∥ ≤ C * ∥f x∥ :=
+begin
+  obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ) (H : ε > 0), ∀ {x y : E}, dist (f x) (f y) < ε → dist x y < 1, from
+    (uniform_embedding_iff.1 hf).2.2 1 zero_lt_one,
+  let δ := ε/2,
+  have δ_pos : δ > 0 := half_pos εpos,
+  have H : ∀{x}, ∥f x∥ ≤ δ → ∥x∥ ≤ 1,
+  { assume x hx,
+    have : dist x 0 ≤ 1,
+    { apply le_of_lt,
+      apply hε,
+      simp [dist_eq_norm],
+      exact lt_of_le_of_lt hx (half_lt_self εpos) },
+  simpa using this },
+  rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
+  refine ⟨δ⁻¹ * ∥c∥, (mul_pos (inv_pos δ_pos) ((lt_trans zero_lt_one hc))), (λx, _)⟩,
+  by_cases hx : f x = 0,
+  { have : f x = f 0, by { simp [hx] },
+    have : x = 0 := (uniform_embedding_iff.1 hf).1 this,
+    simp [this] },
+  { rcases rescale_to_shell hc δ_pos hx with ⟨d, hd, dxle, ledx, dinv⟩,
+    have : ∥f (d • x)∥ ≤ δ, by simpa,
+    have : ∥d • x∥ ≤ 1 := H this,
+    calc ∥x∥ = ∥d∥⁻¹ * ∥d • x∥ :
+      by rwa [← normed_field.norm_inv, ← norm_smul, ← mul_smul, inv_mul_cancel, one_smul]
+    ... ≤ ∥d∥⁻¹ * 1 :
+      mul_le_mul_of_nonneg_left this (inv_nonneg.2 (norm_nonneg _))
+    ... ≤ δ⁻¹ * ∥c∥ * ∥f x∥ :
+      by rwa [mul_one] }
+end
+
 end op_norm
 
 /-- The norm of the tensor product of a scalar linear map and of an element of a normed space
@@ -256,3 +379,15 @@ begin
 end
 
 end continuous_linear_map
+
+/-- If both directions in a linear equiv `e` are continuous, then `e` is a uniform embedding. -/
+lemma linear_equiv.uniform_embedding (e : E ≃ₗ[𝕜] F) (h₁ : continuous e) (h₂ : continuous e.symm) :
+  uniform_embedding e :=
+begin
+  rcases linear_map.bound_of_continuous e.symm.to_linear_map h₂ with ⟨C, Cpos, hC⟩,
+  let f : E →L[𝕜] F := { cont := h₁, ..e },
+  apply f.uniform_embedding_of_bound C (λx, _),
+  have : e.symm (e x) = x := linear_equiv.symm_apply_apply _ _,
+  conv_lhs { rw ← this },
+  exact hC _
+end

src/analysis/normed_space/riesz_lemma.lean

@@ -25,22 +25,31 @@ norms, since in general the existence of an element of norm exactly 1
 is not guaranteed. -/
 lemma riesz_lemma {F : subspace 𝕜 E} (hFc : is_closed (F : set E))
   (hF : ∃ x : E, x ∉ F) {r : ℝ} (hr : r < 1) :
-  ∃ x₀ : E, ∀ y : F, r * ∥x₀∥ ≤ ∥x₀ - y∥ :=
-or.cases_on (le_or_lt r 0)
-(λ hle, ⟨0, λ _, by {rw [norm_zero, mul_zero], exact norm_nonneg _}⟩)
-(λ hlt,
-let ⟨x, hx⟩ := hF in
-let d := metric.inf_dist x F in
-have hFn : (F : set E) ≠ ∅, from set.ne_empty_of_mem (submodule.zero F),
-have hdp : 0 < d,
-  from lt_of_le_of_ne metric.inf_dist_nonneg $ λ heq, hx
-  ((metric.mem_iff_inf_dist_zero_of_closed hFc hFn).2 heq.symm),
-have hdlt : d < d / r,
-  from lt_div_of_mul_lt hlt ((mul_lt_iff_lt_one_right hdp).2 hr),
-let ⟨y₀, hy₀F, hxy₀⟩ := metric.exists_dist_lt_of_inf_dist_lt hdlt hFn in
-⟨x - y₀, λ y,
-have hy₀y : (y₀ + y) ∈ F, from F.add hy₀F y.property,
-le_of_lt $ calc
-∥x - y₀ - y∥ = dist x (y₀ + y) : by { rw [sub_sub, dist_eq_norm] }
-...          ≥ d : metric.inf_dist_le_dist_of_mem hy₀y
-...          > _ : by { rw ←dist_eq_norm, exact (lt_div_iff' hlt).1 hxy₀ }⟩)
+  ∃ x₀ : E, x₀ ∉ F ∧ ∀ y ∈ F, r * ∥x₀∥ ≤ ∥x₀ - y∥ :=
+begin
+  classical,
+  obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF,
+  let d := metric.inf_dist x F,
+  have hFn : (F : set E) ≠ ∅, from set.ne_empty_of_mem (submodule.zero F),
+  have hdp : 0 < d,
+    from lt_of_le_of_ne metric.inf_dist_nonneg (λ heq, hx
+    ((metric.mem_iff_inf_dist_zero_of_closed hFc hFn).2 heq.symm)),
+  let r' := max r 2⁻¹,
+  have hr' : r' < 1, by { simp [r', hr], norm_num },
+  have hlt : 0 < r' := lt_of_lt_of_le (by norm_num) (le_max_right r 2⁻¹),
+  have hdlt : d < d / r', from lt_div_of_mul_lt hlt ((mul_lt_iff_lt_one_right hdp).2 hr'),
+  obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' :=
+    metric.exists_dist_lt_of_inf_dist_lt hdlt hFn,
+  have x_ne_y₀ : x - y₀ ∉ F,
+  { by_contradiction h,
+    have : (x - y₀) + y₀ ∈ F, from F.add h hy₀F,
+    simp only [neg_add_cancel_right, sub_eq_add_neg] at this,
+    exact hx this },
+  refine ⟨x - y₀, x_ne_y₀, λy hy, le_of_lt _⟩,
+  have hy₀y : y₀ + y ∈ F, from F.add hy₀F hy,
+  calc
+    r * ∥x - y₀∥ ≤ r' * ∥x - y₀∥ : mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _)
+    ... < d : by { rw ←dist_eq_norm, exact (lt_div_iff' hlt).1 hxy₀ }
+    ... ≤ dist x (y₀ + y) : metric.inf_dist_le_dist_of_mem hy₀y
+    ... = ∥x - y₀ - y∥ : by { rw [sub_sub, dist_eq_norm] }
+end

src/data/real/ennreal.lean

@@ -578,7 +578,7 @@ forall_ennreal.2 $ and.intro
     (assume h, le_top))
   (assume r hr,
     have ((1 / 2 : nnreal) : ennreal) * ⊤ ≤ r :=
-      hr _ (coe_lt_coe.2 ((@nnreal.coe_lt (1/2) 1).2 one_half_lt_one)),
+      hr _ (coe_lt_coe.2 ((@nnreal.coe_lt (1/2) 1).1 one_half_lt_one)),
     have ne : ((1 / 2 : nnreal) : ennreal) ≠ 0,
     begin
       rw [(≠), coe_eq_zero],

src/data/real/nnreal.lean

@@ -20,6 +20,11 @@ namespace nnreal
 
 instance : has_coe ℝ≥0 ℝ := ⟨subtype.val⟩
 
+instance : can_lift ℝ nnreal :=
+{ coe := coe,
+  cond := λ r, r ≥ 0,
+  prf := λ x hx, ⟨⟨x, hx⟩, rfl⟩ }
+
 protected lemma eq {n m : ℝ≥0} : (n : ℝ) = (m : ℝ) → n = m := subtype.eq
 protected lemma eq_iff {n m : ℝ≥0} : (n : ℝ) = (m : ℝ) ↔ n = m :=
 iff.intro nnreal.eq (congr_arg coe)
@@ -84,9 +89,9 @@ lemma smul_coe (r : ℝ≥0) : ∀n, ↑(add_monoid.smul n r) = add_monoid.smul
 instance : decidable_linear_order ℝ≥0 :=
 decidable_linear_order.lift (coe : ℝ≥0 → ℝ) subtype.val_injective (by apply_instance)
 
-protected lemma coe_le {r₁ r₂ : ℝ≥0} : r₁ ≤ r₂ ↔ (r₁ : ℝ) ≤ r₂ := iff.rfl
-protected lemma coe_lt {r₁ r₂ : ℝ≥0} : r₁ < r₂ ↔ (r₁ : ℝ) < r₂ := iff.rfl
-protected lemma coe_pos {r : ℝ≥0} : 0 < r ↔ (0 : ℝ) < r := iff.rfl
+@[elim_cast] protected lemma coe_le {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) ≤ r₂ ↔ r₁ ≤ r₂ := iff.rfl
+@[elim_cast] protected lemma coe_lt {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) < r₂ ↔ r₁ < r₂ := iff.rfl
+@[elim_cast] protected lemma coe_pos {r : ℝ≥0} : (0 : ℝ) < r ↔ 0 < r := iff.rfl
 
 instance : order_bot ℝ≥0 :=
 { bot := ⊥, bot_le := assume ⟨a, h⟩, h, .. nnreal.decidable_linear_order }
@@ -202,7 +207,7 @@ iff.intro
   (assume (h : (↑a:ℝ) < (↑b:ℝ)),
     let ⟨q, haq, hqb⟩ := exists_rat_btwn h in
     have 0 ≤ (q : ℝ), from le_trans a.2 $ le_of_lt haq,
-    ⟨q, rat.cast_nonneg.1 this, by simp [coe_of_real _ this, nnreal.coe_lt, haq, hqb]⟩)
+    ⟨q, rat.cast_nonneg.1 this, by simp [coe_of_real _ this, nnreal.coe_lt.symm, haq, hqb]⟩)
   (assume ⟨q, _, haq, hqb⟩, lt_trans haq hqb)
 
 lemma bot_eq_zero : (⊥ : nnreal) = 0 := rfl
@@ -233,7 +238,7 @@ by simp [nnreal.of_real]; refl
 by simp [nnreal.of_real, max_eq_left (zero_le_one : (0 :ℝ) ≤ 1)]; refl
 
 @[simp] lemma of_real_pos {r : ℝ} : 0 < nnreal.of_real r ↔ 0 < r :=
-by simp [nnreal.of_real, nnreal.coe_lt, lt_irrefl]
+by simp [nnreal.of_real, nnreal.coe_lt.symm, lt_irrefl]
 
 @[simp] lemma of_real_eq_zero {r : ℝ} : nnreal.of_real r = 0 ↔ r ≤ 0 :=
 by simpa [-of_real_pos] using (not_iff_not.2 (@of_real_pos r))
@@ -246,11 +251,11 @@ nnreal.eq $ by simp [nnreal.of_real]
 
 @[simp] lemma of_real_le_of_real_iff {r p : ℝ} (hp : 0 ≤ p) :
   nnreal.of_real r ≤ nnreal.of_real p ↔ r ≤ p :=
-by simp [nnreal.coe_le, nnreal.of_real, hp]
+by simp [nnreal.coe_le.symm, nnreal.of_real, hp]
 
 @[simp] lemma of_real_lt_of_real_iff' {r p : ℝ} :
   nnreal.of_real r < nnreal.of_real p ↔ r < p ∧ 0 < p :=
-by simp [nnreal.coe_lt, nnreal.of_real, lt_irrefl]
+by simp [nnreal.coe_lt.symm, nnreal.of_real, lt_irrefl]
 
 lemma of_real_lt_of_real_iff {r p : ℝ} (h : 0 < p) :
   nnreal.of_real r < nnreal.of_real p ↔ r < p :=
@@ -268,27 +273,27 @@ lemma of_real_le_of_real {r p : ℝ} (h : r ≤ p) : nnreal.of_real r ≤ nnreal
 nnreal.coe_le.2 $ max_le_max h $ le_refl _
 
 lemma of_real_add_le {r p : ℝ} : nnreal.of_real (r + p) ≤ nnreal.of_real r + nnreal.of_real p :=
-nnreal.coe_le.2 $ max_le (add_le_add (le_max_left _ _) (le_max_left _ _)) nnreal.zero_le_coe
+nnreal.coe_le.1 $ max_le (add_le_add (le_max_left _ _) (le_max_left _ _)) nnreal.zero_le_coe
 
 lemma of_real_le_iff_le_coe {r : ℝ} {p : nnreal} : nnreal.of_real r ≤ p ↔ r ≤ ↑p :=
 begin
   cases le_total 0 r,
-  { rw [nnreal.coe_le, nnreal.coe_of_real r h] },
+  { rw [← nnreal.coe_le, nnreal.coe_of_real r h] },
   { rw [of_real_eq_zero.2 h], split,
     intro, exact le_trans h (coe_nonneg _),
     intro, exact zero_le _ }
 end
 
 lemma le_of_real_iff_coe_le {r : nnreal} {p : ℝ} (hp : p ≥ 0) : r ≤ nnreal.of_real p ↔ ↑r ≤ p :=
-by rw [nnreal.coe_le, nnreal.coe_of_real p hp]
+by rw [← nnreal.coe_le, nnreal.coe_of_real p hp]
 
 lemma of_real_lt_iff_lt_coe {r : ℝ} {p : nnreal} (ha : r ≥ 0) : nnreal.of_real r < p ↔ r < ↑p :=
-by rw [nnreal.coe_lt, nnreal.coe_of_real r ha]
+by rw [← nnreal.coe_lt, nnreal.coe_of_real r ha]
 
 lemma lt_of_real_iff_coe_lt {r : nnreal} {p : ℝ} : r < nnreal.of_real p ↔ ↑r < p :=
 begin
   cases le_total 0 p,
-  { rw [nnreal.coe_lt, nnreal.coe_of_real p h] },
+  { rw [← nnreal.coe_lt, nnreal.coe_of_real p h] },
   { rw [of_real_eq_zero.2 h], split,
     intro, have := not_lt_of_le (zero_le r), contradiction,
     intro rp, have : ¬(p ≤ 0) := not_le_of_lt (lt_of_le_of_lt (coe_nonneg _) rp), contradiction }
@@ -328,13 +333,13 @@ assume hr hp,
 begin
   cases le_total r p,
   { rwa [sub_eq_zero h] },
-  { rw [nnreal.coe_lt, nnreal.coe_sub _ _ h], exact sub_lt_self _ hp }
+  { rw [← nnreal.coe_lt, nnreal.coe_sub _ _ h], exact sub_lt_self _ hp }
 end
 
 @[simp] lemma sub_le_iff_le_add {r p q : nnreal} : r - p ≤ q ↔ r ≤ q + p :=
 match le_total p r with
 | or.inl h :=
-  by rw [nnreal.coe_le, nnreal.coe_le, nnreal.coe_sub _ _ h, nnreal.coe_add, sub_le_iff_le_add]
+  by rw [← nnreal.coe_le, ← nnreal.coe_le, nnreal.coe_sub _ _ h, nnreal.coe_add, sub_le_iff_le_add]
 | or.inr h :=
   have r ≤ p + q, from le_add_right h,
   by simpa [nnreal.coe_le, nnreal.coe_le, sub_eq_zero h]
@@ -401,7 +406,7 @@ eq.symm $ right_distrib a b (c⁻¹)
 lemma add_halves (a : ℝ≥0) : a / 2 + a / 2 = a := nnreal.eq (add_halves a)
 
 lemma half_lt_self {a : ℝ≥0} (h : a ≠ 0) : a / 2 < a :=
-by rw [nnreal.coe_lt, nnreal.coe_div]; exact
+by rw [← nnreal.coe_lt, nnreal.coe_div]; exact
 half_lt_self (bot_lt_iff_ne_bot.2 h)
 
 end inv