chore(nnreal): rename lemmas based on real.to_nnreal when they mentio…

…n of_real (#12937)

Many lemma using `real.to_nnreal` mention `of_real` in their names. This PR tries to make things more coherent.

src/analysis/special_functions/pow.lean

@@ -1114,7 +1114,7 @@ begin
     rw [coe_rpow, real.coe_to_nnreal _ (real.rpow_nonneg_of_nonneg p.1.2 _)],
     refl },
   rw this,
-  refine nnreal.continuous_of_real.continuous_at.comp (continuous_at.comp _ _),
+  refine continuous_real_to_nnreal.continuous_at.comp (continuous_at.comp _ _),
   { apply real.continuous_at_rpow,
     simp at h,
     rw ← (nnreal.coe_eq_zero x) at h,

src/data/real/sqrt.lean

@@ -141,7 +141,7 @@ by rw [real.sqrt, real.to_nnreal_coe]
 
 @[continuity]
 lemma continuous_sqrt : continuous sqrt :=
-nnreal.continuous_coe.comp $ nnreal.sqrt.continuous.comp nnreal.continuous_of_real
+nnreal.continuous_coe.comp $ nnreal.sqrt.continuous.comp continuous_real_to_nnreal
 
 theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : sqrt x = 0 :=
 by simp [sqrt, real.to_nnreal_eq_zero.2 h]

src/measure_theory/constructions/borel_space.lean

@@ -1494,7 +1494,7 @@ variable [measurable_space α]
 
 @[measurability]
 lemma measurable_real_to_nnreal : measurable (real.to_nnreal) :=
-nnreal.continuous_of_real.measurable
+continuous_real_to_nnreal.measurable
 
 @[measurability]
 lemma measurable.real_to_nnreal {f : α → ℝ} (hf : measurable f) :

src/topology/instances/ennreal.lean

@@ -107,7 +107,7 @@ lemma nhds_coe_coe {r p : ℝ≥0} :
 ((open_embedding_coe.prod open_embedding_coe).map_nhds_eq (r, p)).symm
 
 lemma continuous_of_real : continuous ennreal.of_real :=
-(continuous_coe_iff.2 continuous_id).comp nnreal.continuous_of_real
+(continuous_coe_iff.2 continuous_id).comp continuous_real_to_nnreal
 
 lemma tendsto_of_real {f : filter α} {m : α → ℝ} {a : ℝ} (h : tendsto m f (𝓝 a)) :
   tendsto (λa, ennreal.of_real (m a)) f (𝓝 (ennreal.of_real a)) :=
@@ -1067,7 +1067,8 @@ end
 
 lemma ennreal.of_real_tsum_of_nonneg {f : α → ℝ} (hf_nonneg : ∀ n, 0 ≤ f n) (hf : summable f) :
   ennreal.of_real (∑' n, f n) = ∑' n, ennreal.of_real (f n) :=
-by simp_rw [ennreal.of_real, ennreal.tsum_coe_eq (nnreal.has_sum_of_real_of_nonneg hf_nonneg hf)]
+by simp_rw [ennreal.of_real, ennreal.tsum_coe_eq
+  (nnreal.has_sum_real_to_nnreal_of_nonneg hf_nonneg hf)]
 
 lemma not_summable_iff_tendsto_nat_at_top_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
   ¬ summable f ↔ tendsto (λ n : ℕ, ∑ i in finset.range n, f i) at_top at_top :=

src/topology/instances/nnreal.lean

@@ -67,7 +67,7 @@ section coe
 variable {α : Type*}
 open filter finset
 
-lemma continuous_of_real : continuous real.to_nnreal :=
+lemma _root_.continuous_real_to_nnreal : continuous real.to_nnreal :=
 continuous_subtype_mk _ $ continuous_id.max continuous_const
 
 lemma continuous_coe : continuous (coe : ℝ≥0 → ℝ) :=
@@ -91,9 +91,9 @@ lemma comap_coe_at_top : comap (coe : ℝ≥0 → ℝ) at_top = at_top :=
   tendsto (λ a, (m a : ℝ)) f at_top ↔ tendsto m f at_top :=
 tendsto_Ici_at_top.symm
 
-lemma tendsto_of_real {f : filter α} {m : α → ℝ} {x : ℝ} (h : tendsto m f (𝓝 x)) :
+lemma tendsto_real_to_nnreal {f : filter α} {m : α → ℝ} {x : ℝ} (h : tendsto m f (𝓝 x)) :
   tendsto (λa, real.to_nnreal (m a)) f (𝓝 (real.to_nnreal x)) :=
-(continuous_of_real.tendsto _).comp h
+(continuous_real_to_nnreal.tendsto _).comp h
 
 lemma nhds_zero : 𝓝 (0 : ℝ≥0) = ⨅a ≠ 0, 𝓟 (Iio a) :=
 nhds_bot_order.trans $ by simp [bot_lt_iff_ne_bot]
@@ -118,13 +118,13 @@ instance : has_continuous_smul ℝ≥0 ℝ :=
   has_sum (λa, (f a : ℝ)) (r : ℝ) ↔ has_sum f r :=
 by simp only [has_sum, coe_sum.symm, tendsto_coe]
 
-lemma has_sum_of_real_of_nonneg {f : α → ℝ} (hf_nonneg : ∀ n, 0 ≤ f n) (hf : summable f) :
+lemma has_sum_real_to_nnreal_of_nonneg {f : α → ℝ} (hf_nonneg : ∀ n, 0 ≤ f n) (hf : summable f) :
   has_sum (λ n, real.to_nnreal (f n)) (real.to_nnreal (∑' n, f n)) :=
 begin
   have h_sum : (λ s, ∑ b in s, real.to_nnreal (f b)) = λ s, real.to_nnreal (∑ b in s, f b),
     from funext (λ _, (real.to_nnreal_sum_of_nonneg (λ n _, hf_nonneg n)).symm),
   simp_rw [has_sum, h_sum],
-  exact tendsto_of_real hf.has_sum,
+  exact tendsto_real_to_nnreal hf.has_sum,
 end
 
 @[norm_cast] lemma summable_coe {f : α → ℝ≥0} : summable (λa, (f a : ℝ)) ↔ summable f :=
@@ -198,7 +198,7 @@ lemma tendsto_cofinite_zero_of_summable {α} {f : α → ℝ≥0} (hf : summable
 begin
   have h_f_coe : f = λ n, real.to_nnreal (f n : ℝ), from funext (λ n, real.to_nnreal_coe.symm),
   rw [h_f_coe, ← @real.to_nnreal_coe 0],
-  exact tendsto_of_real ((summable_coe.mpr hf).tendsto_cofinite_zero),
+  exact tendsto_real_to_nnreal ((summable_coe.mpr hf).tendsto_cofinite_zero),
 end
 
 lemma tendsto_at_top_zero_of_summable {f : ℕ → ℝ≥0} (hf : summable f) :