feat(EReal): add lemmas (#25011)

Also protect some lemmas.
This branch was cherry-picked from #24916.

Author: urkud

Mathlib/Data/EReal/Basic.lean

@@ -620,6 +620,9 @@ instance : CanLift EReal ℝ≥0∞ (↑) (0 ≤ ·) := ⟨range_coe_ennreal.ge
 theorem coe_ennreal_pos {x : ℝ≥0∞} : (0 : EReal) < x ↔ 0 < x := by
   rw [← coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]
 
+theorem coe_ennreal_pos_iff_ne_zero {x : ℝ≥0∞} : (0 : EReal) < x ↔ x ≠ 0 := by
+  rw [coe_ennreal_pos, pos_iff_ne_zero]
+
 @[simp]
 theorem bot_lt_coe_ennreal (x : ℝ≥0∞) : (⊥ : EReal) < x :=
   (bot_lt_coe 0).trans_le (coe_ennreal_nonneg _)
@@ -687,6 +690,10 @@ lemma toENNReal_eq_zero_iff {x : EReal} : x.toENNReal = 0 ↔ x ≤ 0 := by
 lemma toENNReal_ne_zero_iff {x : EReal} : x.toENNReal ≠ 0 ↔ 0 < x := by
   simp [toENNReal_eq_zero_iff.not]
 
+@[simp]
+lemma toENNReal_pos_iff {x : EReal} : 0 < x.toENNReal ↔ 0 < x := by
+  rw [pos_iff_ne_zero, toENNReal_ne_zero_iff]
+
 @[simp]
 lemma coe_toENNReal {x : EReal} (hx : 0 ≤ x) : (x.toENNReal : EReal) = x := by
   rw [toENNReal]

Mathlib/Data/EReal/Inv.lean

@@ -455,7 +455,7 @@ lemma div_nonneg (h : 0 ≤ a) (h' : 0 ≤ b) : 0 ≤ a / b :=
   mul_nonneg h (inv_nonneg_of_nonneg h')
 
 lemma div_pos (ha : 0 < a) (hb : 0 < b) (hb' : b ≠ ⊤) : 0 < a / b :=
-  mul_pos ha (inv_pos_of_pos_ne_top hb hb')
+  EReal.mul_pos ha (inv_pos_of_pos_ne_top hb hb')
 
 lemma div_nonpos_of_nonpos_of_nonneg (h : a ≤ 0) (h' : 0 ≤ b) : a / b ≤ 0 :=
   mul_nonpos_of_nonpos_of_nonneg h (inv_nonneg_of_nonneg h')

Mathlib/Data/EReal/Operations.lean

@@ -93,17 +93,19 @@ theorem add_top_of_ne_bot {x : EReal} (h : x ≠ ⊥) : x + ⊤ = ⊤ := by
 if and only if `x` is not `⊥`. -/
 theorem add_top_iff_ne_bot {x : EReal} : x + ⊤ = ⊤ ↔ x ≠ ⊥ := by rw [add_comm, top_add_iff_ne_bot]
 
+protected theorem add_pos_of_nonneg_of_pos {a b : EReal} (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b := by
+  lift a to ℝ≥0∞ using ha
+  lift b to ℝ≥0∞ using hb.le
+  norm_cast at *
+  simp [hb]
+
+protected theorem add_pos_of_pos_of_nonneg {a b : EReal} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b :=
+  add_comm a b ▸ EReal.add_pos_of_nonneg_of_pos hb ha
+
 /-- For any two extended real numbers `a` and `b`, if both `a` and `b` are greater than `0`,
 then their sum is also greater than `0`. -/
-theorem add_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a + b := by
-  induction a
-  · exfalso; exact not_lt_bot ha
-  · induction b
-    · exfalso; exact not_lt_bot hb
-    · norm_cast at *; exact Left.add_pos ha hb
-    · exact add_top_of_ne_bot (bot_lt_zero.trans ha).ne' ▸ hb
-  · rw [top_add_of_ne_bot (bot_lt_zero.trans hb).ne']
-    exact ha
+protected theorem add_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a + b :=
+  EReal.add_pos_of_nonneg_of_pos ha.le hb
 
 @[simp]
 theorem coe_add_top (x : ℝ) : (x : EReal) + ⊤ = ⊤ :=
@@ -294,6 +296,11 @@ protected theorem neg_lt_of_neg_lt {a b : EReal} (h : -a < b) : -b < a := neg_lt
 theorem lt_neg_comm {a b : EReal} : a < -b ↔ b < -a := by
   rw [← neg_lt_neg_iff, neg_neg]
 
+@[simp] protected theorem neg_lt_zero {a : EReal} : -a < 0 ↔ 0 < a := by rw [neg_lt_comm, neg_zero]
+@[simp] protected theorem neg_le_zero {a : EReal} : -a ≤ 0 ↔ 0 ≤ a := by rw [EReal.neg_le, neg_zero]
+@[simp] protected theorem neg_pos {a : EReal} : 0 < -a ↔ a < 0 := by rw [lt_neg_comm, neg_zero]
+@[simp] protected theorem neg_nonneg {a : EReal} : 0 ≤ -a ↔ a ≤ 0 := by rw [EReal.le_neg, neg_zero]
+
 /-- If `a < -b` then `b < -a` on `EReal`. -/
 protected theorem lt_neg_of_lt_neg {a b : EReal} (h : a < -b) : b < -a := lt_neg_comm.mp h
 
@@ -313,6 +320,31 @@ lemma neg_sub {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊥) (h2 : x ≠ ⊤ ∨ y
     - (x - y) = - x + y := by
   rw [sub_eq_add_neg, neg_add _ _, sub_eq_add_neg, neg_neg] <;> simp_all
 
+/-- Induction principle for `EReal`s splitting into cases `↑(x : ℝ≥0∞)` and `-↑(x : ℝ≥0∞)`.
+In the latter case, we additionally assume `0 < x`. -/
+@[elab_as_elim]
+def recENNReal {motive : EReal → Sort*} (coe : ∀ x : ℝ≥0∞, motive x)
+    (neg_coe : ∀ x : ℝ≥0∞, 0 < x → motive (-x)) (x : EReal) : motive x :=
+  if hx : 0 ≤ x then coe_toENNReal hx ▸ coe _
+  else
+    have H₁ : 0 < -x := by simpa using hx
+    have H₂ : x = -(-x).toENNReal := by rw [coe_toENNReal H₁.le, neg_neg]
+    H₂ ▸ neg_coe _ <| by simp [H₁]
+
+@[simp]
+theorem recENNReal_coe_ennreal {motive : EReal → Sort*} (coe : ∀ x : ℝ≥0∞, motive x)
+    (neg_coe : ∀ x : ℝ≥0∞, 0 < x → motive (-x)) (x : ℝ≥0∞) : recENNReal coe neg_coe x = coe x := by
+  suffices ∀ y : EReal, x = y → HEq (recENNReal coe neg_coe y : motive y) (coe x) from
+    heq_iff_eq.mp (this x rfl)
+  intro y hy
+  have H₁ : 0 ≤ y := hy ▸ coe_ennreal_nonneg x
+  obtain rfl : y.toENNReal = x := by simp [← hy]
+  simp [recENNReal, H₁]
+
+proof_wanted recENNReal_neg_coe_ennreal {motive : EReal → Sort*} (coe : ∀ x : ℝ≥0∞, motive x)
+    (neg_coe : ∀ x : ℝ≥0∞, 0 < x → motive (-x)) {x : ℝ≥0∞} (hx : 0 < x) :
+    recENNReal coe neg_coe (-x) = neg_coe x hx
+
 /-!
 ### Subtraction
 
@@ -639,8 +671,11 @@ lemma mul_nonneg_iff {a b : EReal} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a 
   rcases lt_trichotomy a 0 with (h | h | h) <;> rcases lt_trichotomy b 0 with (h' | h' | h')
     <;> simp only [h, h', true_or, true_and, or_true, and_true] <;> tauto
 
+protected lemma mul_nonneg {a b : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b :=
+  mul_nonneg_iff.mpr <| .inl ⟨ha, hb⟩
+
 /-- The product of two positive extended real numbers is positive. -/
-lemma mul_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a * b :=
+protected lemma mul_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a * b :=
   mul_pos_iff.mpr (Or.inl ⟨ha, hb⟩)
 
 /-- Induct on two ereals by performing case splits on the sign of one whenever the other is
@@ -772,38 +807,14 @@ lemma toENNReal_mul' {x y : EReal} (hy : 0 ≤ y) :
 
 lemma right_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :
     (a + b) * c = a * c + b * c := by
-  rcases eq_or_lt_of_le ha with (rfl | a_pos)
-  · simp
-  rcases eq_or_lt_of_le hb with (rfl | b_pos)
-  · simp
-  rcases lt_trichotomy c 0 with (c_neg | rfl | c_pos)
-  · induction c
-    · rw [mul_bot_of_pos a_pos, mul_bot_of_pos b_pos, mul_bot_of_pos (add_pos a_pos b_pos),
-        add_bot ⊥]
-    · induction a
-      · exfalso; exact not_lt_bot a_pos
-      · induction b
-        · norm_cast
-        · norm_cast; exact right_distrib _ _ _
-        · norm_cast
-          rw [add_top_of_ne_bot (coe_ne_bot _), top_mul_of_neg c_neg, add_bot]
-      · rw [top_add_of_ne_bot (ne_bot_of_gt b_pos), top_mul_of_neg c_neg, bot_add]
-    · exfalso; exact not_top_lt c_neg
-  · simp
-  · induction c
-    · exfalso; exact not_lt_bot c_pos
-    · induction a
-      · exfalso; exact not_lt_bot a_pos
-      · induction b
-        · norm_cast
-        · norm_cast; exact right_distrib _ _ _
-        · norm_cast
-          rw [add_top_of_ne_bot (coe_ne_bot _), top_mul_of_pos c_pos,
-            add_top_of_ne_bot (coe_ne_bot _)]
-      · rw [top_add_of_ne_bot (ne_bot_of_gt b_pos), top_mul_of_pos c_pos,
-          top_add_of_ne_bot (ne_bot_of_gt (mul_pos b_pos c_pos))]
-    · rw [mul_top_of_pos a_pos, mul_top_of_pos b_pos, mul_top_of_pos (add_pos a_pos b_pos),
-        top_add_top]
+  lift a to ℝ≥0∞ using ha
+  lift b to ℝ≥0∞ using hb
+  cases c using recENNReal with
+  | coe c => exact_mod_cast add_mul a b c
+  | neg_coe c hc =>
+    simp only [mul_neg, ← coe_ennreal_add, ← coe_ennreal_mul, add_mul]
+    rw [coe_ennreal_add, EReal.neg_add (.inl (coe_ennreal_ne_bot _)) (.inr (coe_ennreal_ne_bot _)),
+      sub_eq_add_neg]
 
 lemma left_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :
     c * (a + b) = c * a + c * b := by