chore(data/real/ennreal, measure_theory/): use ≠ ∞ and ≠ 0 in ass…

…umptions (#9219)

src/algebra/big_operators/order.lean

@@ -459,14 +459,16 @@ open finset
 
 /-- A product of finite numbers is still finite -/
 lemma prod_lt_top [canonically_ordered_comm_semiring R] [nontrivial R] [decidable_eq R]
-  {s : finset ι} {f : ι → with_top R} (h : ∀ i ∈ s, f i < ⊤) :
+  {s : finset ι} {f : ι → with_top R} (h : ∀ i ∈ s, f i ≠ ⊤) :
   ∏ i in s, f i < ⊤ :=
-prod_induction f (λ a, a < ⊤) (λ a b, mul_lt_top) (coe_lt_top 1) h
+prod_induction f (λ a, a < ⊤) (λ a b h₁ h₂, mul_lt_top h₁.ne h₂.ne) (coe_lt_top 1) $
+  λ a ha, lt_top_iff_ne_top.2 (h a ha)
 
 /-- A sum of finite numbers is still finite -/
-lemma sum_lt_top [ordered_add_comm_monoid M] {s : finset ι} {f : ι → with_top M} :
-  (∀ i ∈ s, f i < ⊤) → (∑ i in s, f i) < ⊤ :=
-sum_induction f (λ a, a < ⊤) (by { simp_rw add_lt_top, tauto }) zero_lt_top
+lemma sum_lt_top [ordered_add_comm_monoid M] {s : finset ι} {f : ι → with_top M}
+  (h : ∀ i ∈ s, f i ≠ ⊤) : (∑ i in s, f i) < ⊤ :=
+sum_induction f (λ a, a < ⊤) (λ a b h₁ h₂, add_lt_top.2 ⟨h₁, h₂⟩) zero_lt_top $
+  λ i hi, lt_top_iff_ne_top.2 (h i hi)
 
 /-- A sum of numbers is infinite iff one of them is infinite -/
 lemma sum_eq_top_iff [ordered_add_comm_monoid M] {s : finset ι} {f : ι → with_top M} :
@@ -475,7 +477,7 @@ begin
   classical,
   split,
   { contrapose!,
-    exact λ h, (sum_lt_top $ λ i hi, lt_top_iff_ne_top.2 (h i hi)).ne },
+    exact λ h, (sum_lt_top $ λ i hi, (h i hi)).ne },
   { rintro ⟨i, his, hi⟩,
     rw [sum_eq_add_sum_diff_singleton his, hi, top_add] }
 end

src/algebra/ordered_ring.lean

@@ -1434,7 +1434,7 @@ end
 /-- A version of `zero_lt_one : 0 < 1` for a `canonically_ordered_comm_semiring`. -/
 lemma zero_lt_one [nontrivial α] : (0:α) < 1 := (zero_le 1).lt_of_ne zero_ne_one
 
-lemma mul_pos : 0 < a * b ↔ (0 < a) ∧ (0 < b) :=
+@[simp] lemma mul_pos : 0 < a * b ↔ (0 < a) ∧ (0 < b) :=
 by simp only [pos_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
 
 variables [has_sub α] [has_ordered_sub α] [contravariant_class α α (+) (≤)] [is_total α (≤)]
@@ -1514,10 +1514,10 @@ begin
   { simp [← coe_mul] }
 end
 
-lemma mul_lt_top [partial_order α] {a b : with_top α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤ :=
+lemma mul_lt_top [partial_order α] {a b : with_top α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b < ⊤ :=
 begin
-  lift a to α using ne_top_of_lt ha,
-  lift b to α using ne_top_of_lt hb,
+  lift a to α using ha,
+  lift b to α using hb,
   simp only [← coe_mul, coe_lt_top]
 end
 

src/analysis/convex/integral.lean

@@ -64,7 +64,7 @@ begin
   refine hsc.mem_of_tendsto (tendsto_const_nhds.smul this) (eventually_of_forall $ λ n, _),
   have : ∑ y in (F n).range, (μ ((F n) ⁻¹' {y})).to_real = (μ univ).to_real,
     by rw [← (F n).sum_range_measure_preimage_singleton, @ennreal.to_real_sum _ _
-      (λ y, μ ((F n) ⁻¹' {y})) (λ _ _, (measure_lt_top _ _))],
+      (λ y, μ ((F n) ⁻¹' {y})) (λ _ _, (measure_ne_top _ _))],
   rw [← this, simple_func.integral],
   refine hs.center_mass_mem (λ _ _, ennreal.to_real_nonneg) _ _,
   { rw [this, ennreal.to_real_pos_iff, pos_iff_ne_zero, ne.def, measure.measure_univ_eq_zero],

src/analysis/mean_inequalities.lean

@@ -270,17 +270,15 @@ begin
     -- by using `nnreal.rpow_arith_mean_le_arith_mean_rpow`.
     intros h_top_rpow_sum _,
     -- show hypotheses needed to put the `.to_nnreal` inside the sums.
-    have h_top : ∀ (a : ι), a ∈ s → w a * z a < ⊤,
-    { have h_top_sum : ∑ (i : ι) in s, w i * z i < ⊤,
-      { by_contra h,
-        rw [lt_top_iff_ne_top, not_not] at h,
+    have h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤,
+    { have h_top_sum : ∑ (i : ι) in s, w i * z i ≠ ⊤,
+      { intro h,
         rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum,
         exact h_top_rpow_sum rfl, },
-      rwa sum_lt_top_iff at h_top_sum, },
-    have h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p < ⊤,
+      exact λ a ha, (lt_top_of_sum_ne_top h_top_sum ha).ne },
+    have h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤,
     { intros i hi,
       specialize h_top i hi,
-      rw lt_top_iff_ne_top at h_top ⊢,
       rwa [ne.def, ←h_top_iff_rpow_top i hi], },
     -- put the `.to_nnreal` inside the sums.
     simp_rw [to_nnreal_sum h_top_rpow, ←to_nnreal_rpow, to_nnreal_sum h_top, to_nnreal_mul,
@@ -290,11 +288,10 @@ begin
       _ hp,
     -- verify the hypothesis `∑ i in s, (w i).to_nnreal = 1`, using `∑ i in s, w i = 1` .
     have h_sum_nnreal : (∑ i in s, w i) = ↑(∑ i in s, (w i).to_nnreal),
-    { have hw_top : ∑ i in s, w i < ⊤, by { rw hw', exact one_lt_top, },
-      rw ←to_nnreal_sum,
-      { rw coe_to_nnreal,
-        rwa ←lt_top_iff_ne_top, },
-      { rwa sum_lt_top_iff at hw_top, }, },
+    { rw coe_finset_sum,
+      refine sum_congr rfl (λ i hi, (coe_to_nnreal _).symm),
+      refine (lt_top_of_sum_ne_top _ hi).ne,
+      exact hw'.symm ▸ ennreal.one_ne_top },
     rwa [←coe_eq_coe, ←h_sum_nnreal], },
 end
 

src/analysis/normed_space/enorm.lean

@@ -158,9 +158,9 @@ def finite_subspace : subspace 𝕜 V :=
 { carrier   := {x | e x < ⊤},
   zero_mem' := by simp,
   add_mem'  := λ x y hx hy, lt_of_le_of_lt (e.map_add_le x y) (ennreal.add_lt_top.2 ⟨hx, hy⟩),
-  smul_mem' := λ c x hx,
+  smul_mem' := λ c x (hx : _ < _),
     calc e (c • x) = nnnorm c * e x : e.map_smul c x
-               ... < ⊤              : ennreal.mul_lt_top ennreal.coe_lt_top hx }
+               ... < ⊤              : ennreal.mul_lt_top ennreal.coe_ne_top hx.ne }
 
 /-- Metric space structure on `e.finite_subspace`. We use `emetric_space.to_metric_space_of_dist`
 to ensure that this definition agrees with `e.emetric_space`. -/
@@ -169,8 +169,7 @@ begin
   letI := e.emetric_space,
   refine emetric_space.to_metric_space_of_dist _ (λ x y, _) (λ x y, rfl),
   change e (x - y) ≠ ⊤,
-  rw [← ennreal.lt_top_iff_ne_top],
-  exact lt_of_le_of_lt (e.map_sub_le x y) (ennreal.add_lt_top.2 ⟨x.2, y.2⟩)
+  exact ne_top_of_le_ne_top (ennreal.add_lt_top.2 ⟨x.2, y.2⟩).ne (e.map_sub_le x y)
 end
 
 lemma finite_dist_eq (x y : e.finite_subspace) : dist x y = (e (x - y)).to_real := rfl

src/analysis/normed_space/pi_Lp.lean

@@ -236,7 +236,7 @@ begin
     (λf g, (∑ (i : ι), (dist (f i) (g i)) ^ p) ^ (1/p)) (λ f g, _) (λ f g, _),
   { simp [pi_Lp.edist, ennreal.rpow_eq_top_iff, asymm pos, pos,
           ennreal.sum_eq_top_iff, edist_ne_top] },
-  { have A : ∀ (i : ι), i ∈ (finset.univ : finset ι) → edist (f i) (g i) ^ p < ⊤ :=
+  { have A : ∀ (i : ι), i ∈ (finset.univ : finset ι) → edist (f i) (g i) ^ p ≠ ⊤ :=
       λ i hi, by simp [lt_top_iff_ne_top, edist_ne_top, le_of_lt pos],
     simp [dist, -one_div, pi_Lp.edist, ← ennreal.to_real_rpow,
           ennreal.to_real_sum A, dist_edist] }
@@ -254,8 +254,8 @@ begin
     (λf g, (∑ (i : ι), (dist (f i) (g i)) ^ p) ^ (1/p)) (λ f g, _) (λ f g, _),
   { simp [pi_Lp.edist, ennreal.rpow_eq_top_iff, asymm pos, pos,
           ennreal.sum_eq_top_iff, edist_ne_top] },
-  { have A : ∀ (i : ι), i ∈ (finset.univ : finset ι) → edist (f i) (g i) ^ p < ⊤ :=
-      λ i hi, by simp [lt_top_iff_ne_top, edist_ne_top, le_of_lt pos],
+  { have A : ∀ (i : ι), i ∈ (finset.univ : finset ι) → edist (f i) (g i) ^ p ≠ ⊤ :=
+      λ i hi, by simp [edist_ne_top, pos.le],
     simp [dist, -one_div, pi_Lp.edist, ← ennreal.to_real_rpow,
           ennreal.to_real_sum A, dist_edist] }
 end

src/analysis/special_functions/pow.lean

@@ -1500,7 +1500,7 @@ lemma rpow_ne_top_of_nonneg {x : ℝ≥0∞} {y : ℝ} (hy0 : 0 ≤ y) (h : x 
 mt (ennreal.rpow_eq_top_of_nonneg x hy0) h
 
 lemma rpow_lt_top_of_nonneg {x : ℝ≥0∞} {y : ℝ} (hy0 : 0 ≤ y) (h : x ≠ ⊤) : x ^ y < ⊤ :=
-ennreal.lt_top_iff_ne_top.mpr (ennreal.rpow_ne_top_of_nonneg hy0 h)
+lt_top_iff_ne_top.mpr (ennreal.rpow_ne_top_of_nonneg hy0 h)
 
 lemma rpow_add {x : ℝ≥0∞} (y z : ℝ) (hx : x ≠ 0) (h'x : x ≠ ⊤) : x ^ (y + z) = x ^ y * x ^ z :=
 begin

src/analysis/specific_limits.lean

@@ -515,7 +515,7 @@ begin
   refine cauchy_seq_of_edist_le_of_tsum_ne_top _ hu _,
   rw [ennreal.tsum_mul_left, ennreal.tsum_geometric],
   refine ennreal.mul_ne_top hC (ennreal.inv_ne_top.2 _),
-  exact ne_of_gt (ennreal.zero_lt_sub_iff_lt.2 hr)
+  exact (ennreal.sub_pos.2 hr).ne'
 end
 
 omit hr hC
@@ -924,9 +924,9 @@ end
 
 namespace nnreal
 
-theorem exists_pos_sum_of_encodable {ε : ℝ≥0} (hε : 0 < ε) (ι) [encodable ι] :
+theorem exists_pos_sum_of_encodable {ε : ℝ≥0} (hε : ε ≠ 0) (ι) [encodable ι] :
   ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ ∃c, has_sum ε' c ∧ c < ε :=
-let ⟨a, a0, aε⟩ := exists_between hε in
+let ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε) in
 let ⟨ε', hε', c, hc, hcε⟩ := pos_sum_of_encodable a0 ι in
 ⟨ λi, ⟨ε' i, le_of_lt $ hε' i⟩, assume i, nnreal.coe_lt_coe.2 $ hε' i,
   ⟨c, has_sum_le (assume i, le_of_lt $ hε' i) has_sum_zero hc ⟩, nnreal.has_sum_coe.1 hc,
@@ -936,21 +936,21 @@ end nnreal
 
 namespace ennreal
 
-theorem exists_pos_sum_of_encodable {ε : ℝ≥0∞} (hε : 0 < ε) (ι) [encodable ι] :
+theorem exists_pos_sum_of_encodable {ε : ℝ≥0∞} (hε : ε ≠ 0) (ι) [encodable ι] :
   ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ ∑' i, (ε' i : ℝ≥0∞) < ε :=
 begin
-  rcases exists_between hε with ⟨r, h0r, hrε⟩,
+  rcases exists_between (pos_iff_ne_zero.2 hε) with ⟨r, h0r, hrε⟩,
   rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, hx⟩,
-  rcases nnreal.exists_pos_sum_of_encodable (coe_lt_coe.1 h0r) ι with ⟨ε', hp, c, hc, hcr⟩,
+  rcases nnreal.exists_pos_sum_of_encodable (coe_pos.1 h0r).ne' ι with ⟨ε', hp, c, hc, hcr⟩,
   exact ⟨ε', hp, (ennreal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩
 end
 
-theorem exists_pos_sum_of_encodable' {ε : ℝ≥0∞} (hε : 0 < ε) (ι) [encodable ι] :
+theorem exists_pos_sum_of_encodable' {ε : ℝ≥0∞} (hε : ε ≠ 0) (ι) [encodable ι] :
   ∃ ε' : ι → ℝ≥0∞, (∀ i, 0 < ε' i) ∧ (∑' i, ε' i) < ε :=
 let ⟨δ, δpos, hδ⟩ := exists_pos_sum_of_encodable hε ι in
   ⟨λ i, δ i, λ i, ennreal.coe_pos.2 (δpos i), hδ⟩
 
-theorem exists_pos_tsum_mul_lt_of_encodable {ε : ℝ≥0∞} (hε : 0 < ε) {ι} [encodable ι]
+theorem exists_pos_tsum_mul_lt_of_encodable {ε : ℝ≥0∞} (hε : ε ≠ 0) {ι} [encodable ι]
   (w : ι → ℝ≥0∞) (hw : ∀ i, w i ≠ ∞) :
   ∃ δ : ι → ℝ≥0, (∀ i, 0 < δ i) ∧ ∑' i, (w i * δ i : ℝ≥0∞) < ε :=
 begin