chore(data/real/nnreal): drop some lemmas (#18492)

These lemmas are now available for any semifield, so we don't need them.

All these lemmas are `@[deprecated]` in the Mathlib 4 port and will be removed in the forward-port of this PR.

src/analysis/analytic/composition.lean

@@ -453,7 +453,7 @@ begin
   { rcases p.nnnorm_mul_pow_le_of_lt_radius hrp.2 with ⟨Cp, -, hCp⟩,
     exact ⟨max Cp 1, le_max_right _ _, λ n, (hCp n).trans (le_max_left _ _)⟩ },
   let r0 : ℝ≥0 := (4 * Cp)⁻¹,
-  have r0_pos : 0 < r0 := nnreal.inv_pos.2 (mul_pos zero_lt_four (zero_lt_one.trans_le hCp1)),
+  have r0_pos : 0 < r0 := inv_pos.2 (mul_pos zero_lt_four (zero_lt_one.trans_le hCp1)),
   set r : ℝ≥0 := rp * rq * r0,
   have r_pos : 0 < r := mul_pos (mul_pos rp_pos rq_pos) r0_pos,
   have I : ∀ (i : Σ (n : ℕ), composition n),

src/analysis/calculus/inverse.lean

@@ -561,7 +561,7 @@ begin
   let f'symm := f'.nonlinear_right_inverse_of_surjective h,
   set c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2 with hc,
   have f'symm_pos : 0 < f'symm.nnnorm := f'.nonlinear_right_inverse_of_surjective_nnnorm_pos h,
-  have cpos : 0 < c, by simp [hc, nnreal.half_pos, nnreal.inv_pos, f'symm_pos],
+  have cpos : 0 < c, by simp [hc, half_pos, inv_pos, f'symm_pos],
   obtain ⟨s, s_nhds, hs⟩ : ∃ s ∈ 𝓝 a, approximates_linear_on f f' s c :=
     hf.approximates_deriv_on_nhds (or.inr cpos),
   apply hs.map_nhds_eq f'symm s_nhds (or.inr (nnreal.half_lt_self _)),
@@ -577,7 +577,7 @@ begin
   refine ((nhds_basis_opens a).exists_iff _).1 _,
   exact (λ s t, approximates_linear_on.mono_set),
   exact (hf.approximates_deriv_on_nhds $ f'.subsingleton_or_nnnorm_symm_pos.imp id $
-    λ hf', nnreal.half_pos $ nnreal.inv_pos.2 $ hf')
+    λ hf', half_pos $ inv_pos.2 hf')
 end
 
 include cs
@@ -593,7 +593,7 @@ approximates_linear_on.to_local_homeomorph f
   (classical.some hf.approximates_deriv_on_open_nhds)
   (classical.some_spec hf.approximates_deriv_on_open_nhds).snd
   (f'.subsingleton_or_nnnorm_symm_pos.imp id $ λ hf', nnreal.half_lt_self $ ne_of_gt $
-    nnreal.inv_pos.2 $ hf')
+    inv_pos.2 hf')
   (classical.some_spec hf.approximates_deriv_on_open_nhds).fst.2
 
 variable {f}

src/analysis/normed_space/star/mul.lean

@@ -29,7 +29,7 @@ begin
   { have ha : 0 < ‖a‖₊ := zero_le'.trans_lt hr,
     rw [←inv_inv (‖a‖₊), nnreal.lt_inv_iff_mul_lt (inv_ne_zero ha.ne')] at hr,
     obtain ⟨k, hk₁, hk₂⟩ := normed_field.exists_lt_nnnorm_lt 𝕜 (mul_lt_mul_of_pos_right hr $
-      nnreal.inv_pos.2 ha),
+      inv_pos.2 ha),
     refine ⟨_, ⟨k • star a, _, rfl⟩, _⟩,
     { simpa only [mem_closed_ball_zero_iff, norm_smul, one_mul, norm_star] using
         (nnreal.le_inv_iff_mul_le ha.ne').1 (one_mul ‖a‖₊⁻¹ ▸ hk₂.le : ‖k‖₊ ≤ ‖a‖₊⁻¹) },

src/analysis/specific_limits/basic.lean

@@ -503,7 +503,7 @@ begin
   lift w to ι → ℝ≥0 using hw,
   rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩,
   have : ∀ i, 0 < max 1 (w i), from λ i, zero_lt_one.trans_le (le_max_left _ _),
-  refine ⟨λ i, δ' i / max 1 (w i), λ i, nnreal.div_pos (Hpos _) (this i), _⟩,
+  refine ⟨λ i, δ' i / max 1 (w i), λ i, div_pos (Hpos _) (this i), _⟩,
   refine lt_of_le_of_lt (ennreal.tsum_le_tsum $ λ i, _) Hsum,
   rw [coe_div (this i).ne'],
   refine mul_le_of_le_div' (ennreal.mul_le_mul le_rfl $ ennreal.inv_le_inv.2 _),

src/data/real/nnreal.lean

@@ -579,12 +579,6 @@ lemma sum_div {ι} (s : finset ι) (f : ι → ℝ≥0) (b : ℝ≥0) :
   (∑ i in s, f i) / b = ∑ i in s, (f i / b) :=
 finset.sum_div
 
-@[simp] lemma inv_pos {r : ℝ≥0} : 0 < r⁻¹ ↔ 0 < r := inv_pos
-
-lemma div_pos {r p : ℝ≥0} (hr : 0 < r) (hp : 0 < p) : 0 < r / p := div_pos hr hp
-
-lemma div_self_le (r : ℝ≥0) : r / r ≤ 1 := div_self_le_one r
-
 @[simp] lemma inv_le {r p : ℝ≥0} (h : r ≠ 0) : r⁻¹ ≤ p ↔ 1 ≤ r * p :=
 by rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h]
 
@@ -661,36 +655,16 @@ le_of_forall_ge_of_dense $ assume a ha,
   have (a * x⁻¹) * x ≤ y, from h _ this,
   by rwa [mul_assoc, inv_mul_cancel hx, mul_one] at this
 
-lemma div_add_div_same (a b c : ℝ≥0) : a / c + b / c = (a + b) / c := div_add_div_same _ _ _
-
-lemma half_pos {a : ℝ≥0} (h : 0 < a) : 0 < a / 2 := half_pos h
-
-lemma add_halves (a : ℝ≥0) : a / 2 + a / 2 = a := add_halves _
-
 lemma half_le_self (a : ℝ≥0) : a / 2 ≤ a := half_le_self bot_le
 
 lemma half_lt_self {a : ℝ≥0} (h : a ≠ 0) : a / 2 < a := half_lt_self h.bot_lt
 
-lemma two_inv_lt_one : (2⁻¹:ℝ≥0) < 1 := two_inv_lt_one
-
 lemma div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) : a / b < 1 :=
 begin
   rwa [div_lt_iff, one_mul],
   exact ne_of_gt (lt_of_le_of_lt (zero_le _) h)
 end
 
-@[field_simps] lemma div_add_div (a : ℝ≥0) {b : ℝ≥0} (c : ℝ≥0) {d : ℝ≥0}
-  (hb : b ≠ 0) (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d) :=
-div_add_div _ _ hb hd
-
-@[field_simps] lemma add_div' (a b c : ℝ≥0) (hc : c ≠ 0) :
-  b + a / c = (b * c + a) / c :=
-add_div' _ _ _ hc
-
-@[field_simps] lemma div_add' (a b c : ℝ≥0) (hc : c ≠ 0) :
-  a / c + b = (a + b * c) / c :=
-div_add' _ _ _ hc
-
 lemma _root_.real.to_nnreal_inv {x : ℝ} :
   real.to_nnreal x⁻¹ = (real.to_nnreal x)⁻¹ :=
 begin
@@ -712,19 +686,15 @@ by rw [div_eq_inv_mul, div_eq_inv_mul, real.to_nnreal_mul (inv_nonneg.2 hy), rea
 lemma inv_lt_one_iff {x : ℝ≥0} (hx : x ≠ 0) : x⁻¹ < 1 ↔ 1 < x :=
 by rwa [← one_div, div_lt_iff hx, one_mul]
 
-lemma inv_lt_one {x : ℝ≥0} (hx : 1 < x) : x⁻¹ < 1 := inv_lt_one hx
-
 lemma zpow_pos {x : ℝ≥0} (hx : x ≠ 0) (n : ℤ) : 0 < x ^ n :=
 begin
   cases n,
   { simp [pow_pos hx.bot_lt _] },
   { simp [pow_pos hx.bot_lt _] }
 end
 
-lemma inv_lt_inv_iff {x y : ℝ≥0} (hx : x ≠ 0) (hy : y ≠ 0) : y⁻¹ < x⁻¹ ↔ x < y := inv_lt_inv₀ hy hx
-
 lemma inv_lt_inv {x y : ℝ≥0} (hx : x ≠ 0) (h : x < y) : y⁻¹ < x⁻¹ :=
-(inv_lt_inv_iff hx ((bot_le.trans_lt h).ne')).2 h
+inv_lt_inv_of_lt hx.bot_lt h
 
 end inv
 

src/measure_theory/covering/differentiation.lean

@@ -594,7 +594,7 @@ begin
         conv_rhs { rw ← mul_one (t^ n) },
         refine mul_lt_mul' le_rfl _ (zero_le _) (nnreal.zpow_pos t_ne_zero' _),
         rw zpow_neg_one,
-        exact nnreal.inv_lt_one ht,
+        exact inv_lt_one ht,
       end },
   calc ν s = ν (s ∩ f⁻¹' {0}) + ν (s ∩ f⁻¹' {∞}) + ∑' (n : ℤ), ν (s ∩ f⁻¹' (Ico (t^n) (t^(n+1)))) :
     measure_eq_measure_preimage_add_measure_tsum_Ico_zpow ν f_meas hs ht

src/measure_theory/covering/liminf_limsup.lean

@@ -105,7 +105,7 @@ begin
     replace hη' : 1 ≤ η := by simpa only [ennreal.one_le_coe_iff] using
       le_of_tendsto (hd' w (λ j, r₁ (f j)) hr $ eventually_of_forall hw') hη',
     exact (lt_self_iff_false _).mp (lt_of_lt_of_le hη hη'), },
-  refine ⟨1 - C⁻¹, tsub_lt_self zero_lt_one (nnreal.inv_pos.mpr hC), _⟩,
+  refine ⟨1 - C⁻¹, tsub_lt_self zero_lt_one (inv_pos.mpr hC), _⟩,
   replace hC : C ≠ 0 := ne_of_gt hC,
   let b : ℕ → set α := λ j, closed_ball (w j) (M * r₁ (f j)),
   let B : ℕ → set α := λ j, closed_ball (w j) (r₁ (f j)),

src/measure_theory/decomposition/lebesgue.lean

@@ -429,7 +429,7 @@ begin
     by_cases hb : 0 < νA,
     { suffices : ∀ b, 0 < b → μA ≤ b,
       { by_contra,
-        have h' := this (μA / 2) (nnreal.half_pos (zero_lt_iff.2 h)),
+        have h' := this (μA / 2) (half_pos (zero_lt_iff.2 h)),
         rw ← @not_not (μA ≤ μA / 2) at h',
         exact h' (not_le.2 (nnreal.half_lt_self h)) },
       intros c hc,

src/measure_theory/function/conditional_expectation/real.lean

@@ -212,7 +212,7 @@ begin
   obtain ⟨δ, hδ, h⟩ := hg.snorm_indicator_le μ le_rfl ennreal.one_ne_top hε,
   set C : ℝ≥0 := ⟨δ, hδ.le⟩⁻¹ * (snorm g 1 μ).to_nnreal with hC,
   have hCpos : 0 < C :=
-    mul_pos (nnreal.inv_pos.2 hδ) (ennreal.to_nnreal_pos hne hg.snorm_lt_top.ne),
+    mul_pos (inv_pos.2 hδ) (ennreal.to_nnreal_pos hne hg.snorm_lt_top.ne),
   have : ∀ n, μ {x : α | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ ennreal.of_real δ,
   { intro n,
     have := mul_meas_ge_le_pow_snorm' μ one_ne_zero ennreal.one_ne_top

src/measure_theory/function/jacobian.lean

@@ -415,7 +415,7 @@ begin
     { simp only [h, true_or, eventually_const] },
     simp only [h, false_or],
     apply Iio_mem_nhds,
-    simpa only [h, false_or, nnreal.inv_pos] using B.subsingleton_or_nnnorm_symm_pos },
+    simpa only [h, false_or, inv_pos] using B.subsingleton_or_nnnorm_symm_pos },
   have L2 : ∀ᶠ δ in 𝓝 (0 : ℝ≥0),
     ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀,
   { have : tendsto (λ δ, ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ)

src/measure_theory/integral/riesz_markov_kakutani.lean

@@ -93,9 +93,9 @@ begin
   intros ε εpos,
   --get test functions s.t. `λ(Ki) ≤ Λfi ≤ λ(Ki) + ε/2, i=1,2`
   obtain ⟨f1, f_test_function_K1⟩ := exists_lt_riesz_content_aux_add_pos Λ K1
-    (nnreal.half_pos εpos),
+    (half_pos εpos),
   obtain ⟨f2, f_test_function_K2⟩ := exists_lt_riesz_content_aux_add_pos Λ K2
-    (nnreal.half_pos εpos),
+    (half_pos εpos),
   --let `f := f1 + f2` test function for the content of `K`
   have f_test_function_union : (∀ x ∈ (K1 ⊔ K2), (1 : ℝ≥0) ≤ (f1 + f2) x),
   { rintros x (x_in_K1 | x_in_K2),
@@ -106,7 +106,7 @@ begin
   rw map_add,
   --use that `Λfi` are lower bounds for `λ(Ki) + ε/2`
   apply lt_of_lt_of_le (add_lt_add f_test_function_K1.right f_test_function_K2.right) (le_of_eq _),
-  rw [add_assoc, add_comm (ε/2), add_assoc, nnreal.add_halves ε, add_assoc],
+  rw [add_assoc, add_comm (ε/2), add_assoc, add_halves ε, add_assoc],
 end
 
 end riesz_subadditive

src/topology/metric_space/hausdorff_distance.lean

@@ -1166,7 +1166,7 @@ begin
   refine (h x hx y hy).not_le _,
   calc edist x y ≤ edist z x + edist z y : edist_triangle_left _ _ _
   ... ≤ ↑(r / 2) + ↑(r / 2) : add_le_add hzx.le hzy.le
-  ... = r : by rw [← ennreal.coe_add, nnreal.add_halves]
+  ... = r : by rw [← ennreal.coe_add, add_halves]
 end
 
 lemma _root_.disjoint.exists_cthickenings (hst : disjoint s t) (hs : is_compact s)

src/topology/metric_space/metrizable_uniformity.lean

@@ -199,7 +199,7 @@ begin
   { intros x y, dsimp only [d],
     simp only [@symmetric_rel.mk_mem_comm _ _ (hU_symm _) x y] },
   have hr : (1 / 2 : ℝ≥0) ∈ Ioo (0 : ℝ≥0) 1,
-    from ⟨nnreal.half_pos one_pos, nnreal.half_lt_self one_ne_zero⟩,
+    from ⟨half_pos one_pos, nnreal.half_lt_self one_ne_zero⟩,
   letI I := pseudo_metric_space.of_prenndist d (λ x, hd₀.2 (setoid.refl _)) hd_symm,
   have hdist_le : ∀ x y, dist x y ≤ d x y,
     from pseudo_metric_space.dist_of_prenndist_le _ _ _,