feat(*/with_top): add lemmas about with_top/with_bot (#18487)

Backport leanprover-community/mathlib4#2406

Author: urkud

src/algebra/big_operators/order.lean

@@ -602,34 +602,26 @@ namespace with_top
 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 ≠ ⊤) :
+lemma prod_lt_top [comm_monoid_with_zero R] [no_zero_divisors R] [nontrivial R] [decidable_eq R]
+  [has_lt R] {s : finset ι} {f : ι → with_top R} (h : ∀ i ∈ s, f i ≠ ⊤) :
   ∏ i in s, f i < ⊤ :=
-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}
-  (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)
+prod_induction f (λ a, a < ⊤) (λ a b h₁ h₂, mul_lt_top' h₁ h₂) (coe_lt_top 1) $
+  λ a ha, with_top.lt_top_iff_ne_top.2 (h a ha)
 
 /-- 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} :
+lemma sum_eq_top_iff [add_comm_monoid M] {s : finset ι} {f : ι → with_top M} :
   ∑ i in s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤ :=
-begin
-  classical,
-  split,
-  { contrapose!,
-    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
+by induction s using finset.cons_induction; simp [*, or_and_distrib_right, exists_or_distrib]
 
 /-- A sum of finite numbers is still finite -/
-lemma sum_lt_top_iff [ordered_add_comm_monoid M] {s : finset ι} {f : ι → with_top M} :
+lemma sum_lt_top_iff [add_comm_monoid M] [has_lt M] {s : finset ι} {f : ι → with_top M} :
   ∑ i in s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤ :=
-by simp only [lt_top_iff_ne_top, ne.def, sum_eq_top_iff, not_exists]
+by simp only [with_top.lt_top_iff_ne_top, ne.def, sum_eq_top_iff, not_exists]
+
+/-- A sum of finite numbers is still finite -/
+lemma sum_lt_top [add_comm_monoid M] [has_lt M] {s : finset ι} {f : ι → with_top M}
+  (h : ∀ i ∈ s, f i ≠ ⊤) : (∑ i in s, f i) < ⊤ :=
+sum_lt_top_iff.2 $ λ i hi, with_top.lt_top_iff_ne_top.2 (h i hi)
 
 end with_top
 
@@ -640,13 +632,7 @@ variables {S : Type*}
 lemma absolute_value.sum_le [semiring R] [ordered_semiring S]
   (abv : absolute_value R S) (s : finset ι) (f : ι → R) :
   abv (∑ i in s, f i) ≤ ∑ i in s, abv (f i) :=
-begin
-  letI := classical.dec_eq ι,
-  refine finset.induction_on s _ (λ i s hi ih, _),
-  { simp },
-  { simp only [finset.sum_insert hi],
-  exact (abv.add_le _ _).trans (add_le_add le_rfl ih) },
-end
+finset.le_sum_of_subadditive abv (map_zero _) abv.add_le _ _
 
 lemma is_absolute_value.abv_sum [semiring R] [ordered_semiring S] (abv : R → S)
   [is_absolute_value abv] (f : ι → R) (s : finset ι) :

src/algebra/order/monoid/with_top.lean

@@ -74,8 +74,8 @@ by cases a; cases b; simp [none_eq_top, some_eq_coe, ←with_top.coe_add]
 
 lemma add_ne_top : a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤ := add_eq_top.not.trans not_or_distrib
 
-lemma add_lt_top [partial_order α] {a b : with_top α} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
-by simp_rw [lt_top_iff_ne_top, add_ne_top]
+lemma add_lt_top [has_lt α] {a b : with_top α} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
+by simp_rw [with_top.lt_top_iff_ne_top, add_ne_top]
 
 lemma add_eq_coe : ∀ {a b : with_top α} {c : α},
   a + b = c ↔ ∃ (a' b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
@@ -380,7 +380,7 @@ lemma coe_bit1 [has_one α] {a : α} : ((bit1 a : α) : with_bot α) = bit1 a :=
 @[simp] lemma add_eq_bot : a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥ := with_top.add_eq_top
 lemma add_ne_bot : a + b ≠ ⊥ ↔ a ≠ ⊥ ∧ b ≠ ⊥ := with_top.add_ne_top
 
-lemma bot_lt_add [partial_order α] {a b : with_bot α} : ⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b :=
+lemma bot_lt_add [has_lt α] {a b : with_bot α} : ⊥ < a + b ↔ ⊥ < a ∧ ⊥ < b :=
 @with_top.add_lt_top αᵒᵈ _ _ _ _
 
 lemma add_eq_coe : a + b = x ↔ ∃ (a' b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = x := with_top.add_eq_coe

src/algebra/order/ring/with_top.lean

@@ -36,15 +36,36 @@ instance : mul_zero_class (with_top α) :=
 
 lemma mul_def {a b : with_top α} : a * b = if a = 0 ∨ b = 0 then 0 else option.map₂ (*) a b := rfl
 
-@[simp] lemma mul_top {a : with_top α} (h : a ≠ 0) : a * ⊤ = ⊤ :=
-by cases a; simp [mul_def, h]; refl
+lemma mul_top' {a : with_top α} : a * ⊤ = if a = 0 then 0 else ⊤ :=
+by induction a using with_top.rec_top_coe; simp [mul_def]; refl
 
-@[simp] lemma top_mul {a : with_top α} (h : a ≠ 0) : ⊤ * a = ⊤ :=
-by cases a; simp [mul_def, h]; refl
+@[simp] lemma mul_top {a : with_top α} (h : a ≠ 0) : a * ⊤ = ⊤ := by rw [mul_top', if_neg h]
+
+lemma top_mul' {a : with_top α} : ⊤ * a = if a = 0 then 0 else ⊤ :=
+by induction a using with_top.rec_top_coe; simp [mul_def]; refl
+
+@[simp] lemma top_mul {a : with_top α} (h : a ≠ 0) : ⊤ * a = ⊤ := by rw [top_mul', if_neg h]
 
 @[simp] lemma top_mul_top : (⊤ * ⊤ : with_top α) = ⊤ :=
 top_mul top_ne_zero
 
+theorem mul_eq_top_iff {a b : with_top α} : a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0 :=
+begin
+  rw [mul_def, ite_eq_iff, ← none_eq_top, option.map₂_eq_none_iff],
+  have ha : a = 0 → a ≠ none := λ h, h.symm ▸ zero_ne_top,
+  have hb : b = 0 → b ≠ none := λ h, h.symm ▸ zero_ne_top,
+  tauto
+end
+
+theorem mul_lt_top' [has_lt α] {a b : with_top α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤ :=
+begin
+  rw [with_top.lt_top_iff_ne_top] at *,
+  simp only [ne.def, mul_eq_top_iff, *, and_false, false_and, false_or, not_false_iff]
+end
+
+theorem mul_lt_top [has_lt α] {a b : with_top α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b < ⊤ :=
+  mul_lt_top' (with_top.lt_top_iff_ne_top.2 ha) (with_top.lt_top_iff_ne_top.2 hb)
+
 instance [no_zero_divisors α] : no_zero_divisors (with_top α) :=
 begin
   refine ⟨λ a b h₁, decidable.by_contradiction $ λ h₂, _⟩,
@@ -59,7 +80,7 @@ section mul_zero_class
 
 variables [mul_zero_class α]
 
-@[norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_top α) = a * b :=
+@[simp, norm_cast] lemma coe_mul {a b : α} : (↑(a * b) : with_top α) = a * b :=
 decidable.by_cases (assume : a = 0, by simp [this]) $ assume ha,
 decidable.by_cases (assume : b = 0, by simp [this]) $ assume hb,
 by { simp [*, mul_def] }
@@ -69,22 +90,6 @@ lemma mul_coe {b : α} (hb : b ≠ 0) : ∀{a : with_top α}, a * b = a.bind (λ
     by simp [hb]
 | (some a) := show ↑a * ↑b = ↑(a * b), from coe_mul.symm
 
-@[simp] lemma mul_eq_top_iff {a b : with_top α} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
-begin
-  cases a; cases b; simp only [none_eq_top, some_eq_coe],
-  { simp [← coe_mul] },
-  { by_cases hb : b = 0; simp [hb] },
-  { by_cases ha : a = 0; simp [ha] },
-  { simp [← coe_mul] }
-end
-
-lemma mul_lt_top [preorder α] {a b : with_top α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b < ⊤ :=
-begin
-  lift a to α using ha,
-  lift b to α using hb,
-  simp only [← coe_mul, coe_lt_top]
-end
-
 @[simp] lemma untop'_zero_mul (a b : with_top α) : (a * b).untop' 0 = a.untop' 0 * b.untop' 0 :=
 begin
   by_cases ha : a = 0, { rw [ha, zero_mul, ← coe_zero, untop'_coe, zero_mul] },
@@ -127,7 +132,7 @@ instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_top
       induction y using with_top.rec_top_coe,
       { have : (f x : with_top S) ≠ 0, by simpa [hf.eq_iff' (map_zero f)] using hx,
         simp [hx, this] },
-      simp [← coe_mul]
+      simp only [← coe_mul, map_coe, map_mul]
     end,
   .. f.to_zero_hom.with_top_map, .. f.to_monoid_hom.to_one_hom.with_top_map }
 
@@ -163,7 +168,7 @@ begin
   induction c using with_top.rec_top_coe,
   { by_cases ha : a = 0; simp [ha] },
   { by_cases hc : c = 0, { simp [hc] },
-    simp [mul_coe hc], cases a; cases b,
+    simp only [mul_coe hc], cases a; cases b,
     repeat { refl <|> exact congr_arg some (add_mul _ _ _) } }
 end
 
@@ -216,6 +221,15 @@ with_top.top_mul h
 @[simp] lemma bot_mul_bot : (⊥ * ⊥ : with_bot α) = ⊥ :=
 with_top.top_mul_top
 
+theorem mul_eq_bot_iff {a b : with_bot α} : a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0 :=
+with_top.mul_eq_top_iff
+
+theorem bot_lt_mul' [has_lt α] {a b : with_bot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b :=
+@with_top.mul_lt_top' αᵒᵈ _ _ _ _ _ _ ha hb
+
+theorem bot_lt_mul [has_lt α] {a b : with_bot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : ⊥ < a * b :=
+@with_top.mul_lt_top αᵒᵈ _ _ _ _ _ _ ha hb
+
 end has_mul
 
 section mul_zero_class
@@ -228,16 +242,6 @@ with_top.coe_mul
 lemma mul_coe {b : α} (hb : b ≠ 0) {a : with_bot α} : a * b = a.bind (λa:α, ↑(a * b)) :=
 with_top.mul_coe hb
 
-@[simp] lemma mul_eq_bot_iff {a b : with_bot α} : a * b = ⊥ ↔ (a ≠ 0 ∧ b = ⊥) ∨ (a = ⊥ ∧ b ≠ 0) :=
-with_top.mul_eq_top_iff
-
-lemma bot_lt_mul [preorder α] {a b : with_bot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b :=
-begin
-  lift a to α using ne_bot_of_gt ha,
-  lift b to α using ne_bot_of_gt hb,
-  simp only [← coe_mul, bot_lt_coe],
-end
-
 end mul_zero_class
 
 /-- `nontrivial α` is needed here as otherwise we have `1 * ⊥ = ⊥` but also `= 0 * ⊥ = 0`. -/

src/algebra/order/sub/with_top.lean

@@ -33,6 +33,11 @@ instance : has_sub (with_top α) :=
 @[simp] lemma top_sub_coe {a : α} : (⊤ : with_top α) - a = ⊤ := rfl
 @[simp] lemma sub_top {a : with_top α} : a - ⊤ = 0 := by { cases a; refl }
 
+@[simp] theorem sub_eq_top_iff : ∀ {a b : with_top α}, a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
+| _ ⊤ := by simp
+| ⊤ (b : α) := by simp
+| (a : α) (b : α) := by simp only [← coe_sub, coe_ne_top, false_and]
+
 lemma map_sub [has_sub β] [has_zero β] {f : α → β} (h : ∀ x y, f (x - y) = f x - f y)
   (h₀ : f 0 = 0) :
   ∀ x y : with_top α, (x - y).map f = x.map f - y.map f

src/analysis/bounded_variation.lean

@@ -933,12 +933,7 @@ lemma lipschitz_on_with.comp_has_bounded_variation_on {f : E → F} {C : ℝ≥0
   (hf : lipschitz_on_with C f t) {g : α → E} {s : set α} (hg : maps_to g s t)
   (h : has_bounded_variation_on g s) :
   has_bounded_variation_on (f ∘ g) s :=
-begin
-  dsimp [has_bounded_variation_on] at h,
-  apply ne_of_lt,
-  apply (hf.comp_evariation_on_le hg).trans_lt,
-  simp [lt_top_iff_ne_top, h],
-end
+ne_top_of_le_ne_top (ennreal.mul_ne_top ennreal.coe_ne_top h) (hf.comp_evariation_on_le hg)
 
 lemma lipschitz_on_with.comp_has_locally_bounded_variation_on {f : E → F} {C : ℝ≥0} {t : set E}
   (hf : lipschitz_on_with C f t) {g : α → E} {s : set α} (hg : maps_to g s t)

src/analysis/mean_inequalities_pow.lean

@@ -198,7 +198,7 @@ begin
   have hp_not_nonpos : ¬ p ≤ 0, by simp [hp_pos],
   have hp_not_neg : ¬ p < 0, by simp [hp_nonneg],
   have h_top_iff_rpow_top : ∀ (i : ι) (hi : i ∈ s), w i * z i = ⊤ ↔ w i * (z i) ^ p = ⊤,
-  by simp [hp_pos, hp_nonneg, hp_not_nonpos, hp_not_neg],
+    by simp [ennreal.mul_eq_top, hp_pos, hp_nonneg, hp_not_nonpos, hp_not_neg],
   refine le_of_top_imp_top_of_to_nnreal_le _ _,
   { -- first, prove `(∑ i in s, w i * z i) ^ p = ⊤ → ∑ i in s, (w i * z i ^ p) = ⊤`
     rw [rpow_eq_top_iff, sum_eq_top_iff, sum_eq_top_iff],

src/analysis/p_series.lean

@@ -122,7 +122,7 @@ begin
   split; intro h,
   { replace hf : ∀ m n, 1 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m :=
       λ m n hm hmn, ennreal.coe_le_coe.2 (hf (zero_lt_one.trans hm) hmn),
-    simpa [h, ennreal.add_eq_top] using (ennreal.tsum_condensed_le hf) },
+    simpa [h, ennreal.add_eq_top, ennreal.mul_eq_top] using ennreal.tsum_condensed_le hf },
   { replace hf : ∀ m n, 0 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m :=
       λ m n hm hmn, ennreal.coe_le_coe.2 (hf hm hmn),
     simpa [h, ennreal.add_eq_top] using (ennreal.le_tsum_condensed hf) }

src/data/real/ennreal.lean

@@ -720,35 +720,38 @@ mul_right_mono.map_max
 lemma mul_max : a * max b c = max (a * b) (a * c) :=
 mul_left_mono.map_max
 
-lemma mul_eq_mul_left : a ≠ 0 → a ≠ ∞ → (a * b = a * c ↔ b = c) :=
+theorem mul_left_strictMono (h0 : a ≠ 0) (hinf : a ≠ ∞) : strict_mono ((*) a) :=
 begin
-  cases a; cases b; cases c;
-    simp [none_eq_top, some_eq_coe, mul_top, top_mul, -coe_mul, coe_mul.symm,
-      nnreal.mul_eq_mul_left] {contextual := tt},
+  lift a to ℝ≥0 using hinf,
+  rw [coe_ne_zero] at h0,
+  intros x y h,
+  contrapose! h,
+  simpa only [← mul_assoc, ← coe_mul, inv_mul_cancel h0, coe_one, one_mul]
+    using mul_le_mul' (le_refl ↑a⁻¹) h
 end
 
+lemma mul_eq_mul_left (h₀ : a ≠ 0) (hinf : a ≠ ∞) : a * b = a * c ↔ b = c :=
+(mul_left_strictMono h₀ hinf).injective.eq_iff
+
 lemma mul_eq_mul_right : c ≠ 0 → c ≠ ∞ → (a * c = b * c ↔ a = b) :=
 mul_comm c a ▸ mul_comm c b ▸ mul_eq_mul_left
 
-lemma mul_le_mul_left : a ≠ 0 → a ≠ ∞ → (a * b ≤ a * c ↔ b ≤ c) :=
-begin
-  cases a; cases b; cases c;
-    simp [none_eq_top, some_eq_coe, mul_top, top_mul, -coe_mul, coe_mul.symm] {contextual := tt},
-  assume h, exact mul_le_mul_left (pos_iff_ne_zero.2 h)
-end
+lemma mul_le_mul_left (h₀ : a ≠ 0) (hinf : a ≠ ∞) : a * b ≤ a * c ↔ b ≤ c :=
+(mul_left_strictMono h₀ hinf).le_iff_le
 
 lemma mul_le_mul_right : c ≠ 0 → c ≠ ∞ → (a * c ≤ b * c ↔ a ≤ b) :=
 mul_comm c a ▸ mul_comm c b ▸ mul_le_mul_left
 
-lemma mul_lt_mul_left : a ≠ 0 → a ≠ ∞ → (a * b < a * c ↔ b < c) :=
-λ h0 ht, by simp only [mul_le_mul_left h0 ht, lt_iff_le_not_le]
+lemma mul_lt_mul_left (h₀ : a ≠ 0) (hinf : a ≠ ∞) : a * b < a * c ↔ b < c :=
+(mul_left_strictMono h₀ hinf).lt_iff_lt
 
 lemma mul_lt_mul_right : c ≠ 0 → c ≠ ∞ → (a * c < b * c ↔ a < b) :=
 mul_comm c a ▸ mul_comm c b ▸ mul_lt_mul_left
 
 end mul
 
 section cancel
+
 /-- An element `a` is `add_le_cancellable` if `a + b ≤ a + c` implies `b ≤ c` for all `b` and `c`.
   This is true in `ℝ≥0∞` for all elements except `∞`. -/
 lemma add_le_cancellable_iff_ne {a : ℝ≥0∞} : add_le_cancellable a ↔ a ≠ ∞ :=

src/data/real/ereal.lean

@@ -405,7 +405,8 @@ by cases x; cases y; refl
         exact nnreal.coe_pos.2 (bot_lt_iff_ne_bot.2 h) },
       simp only [coe_nnreal_eq_coe_real, coe_ennreal_top, (*), ereal.mul, A, if_true] }
   end
-| (x : ℝ≥0) (y : ℝ≥0) := by simp [←ennreal.coe_mul, coe_nnreal_eq_coe_real]
+| (x : ℝ≥0) (y : ℝ≥0) := by simp only [← ennreal.coe_mul, coe_nnreal_eq_coe_real,
+    nnreal.coe_mul, ereal.coe_mul]
 
 @[norm_cast] lemma coe_ennreal_nsmul (n : ℕ) (x : ℝ≥0∞) : (↑(n • x) : ereal) = n • x :=
 map_nsmul (⟨coe, coe_ennreal_zero, coe_ennreal_add⟩ : ℝ≥0∞ →+ ereal) _ _

src/measure_theory/function/l1_space.lean

@@ -147,7 +147,8 @@ has_finite_integral_congr' $ h.fun_comp norm
 
 lemma has_finite_integral_const_iff {c : β} :
   has_finite_integral (λ x : α, c) μ ↔ c = 0 ∨ μ univ < ∞ :=
-by simp [has_finite_integral, lintegral_const, lt_top_iff_ne_top, or_iff_not_imp_left]
+by simp [has_finite_integral, lintegral_const, lt_top_iff_ne_top, ennreal.mul_eq_top,
+  or_iff_not_imp_left]
 
 lemma has_finite_integral_const [is_finite_measure μ] (c : β) :
   has_finite_integral (λ x : α, c) μ :=