refactor(EReal): add add/sub lemmas and refactor limsup_add on EReal (#18879)

This PR :

- adds a few lemmas about addition/subtraction in `Topology.Instances.EReal`. These are translations in `EReal` of similar lemmas about multiplication/division in `ENNReal` (see `Data.ENNReal.Inv`).
- renames [EReal.add_le_of_forall_add_le](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/EReal.html#EReal.add_le_of_forall_add_le), [EReal.le_add_of_forall_le_add](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/EReal.html#EReal.le_add_of_forall_le_add) to bring them in line with similar lemmas in `Real`/`ENNReal` (see e.g. [add_le_of_forall_lt](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Group/DenselyOrdered.html#add_le_of_forall_lt))
- simplifies significantly the proofs of `add_le_of_forall_lt` and `le_add_of_forall_lt`.
- renames [EReal.add_liminf_le_liminf_add](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/EReal.html#EReal.add_liminf_le_liminf_add), [EReal.limsup_add_le_add_limsup](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/EReal.html#EReal.limsup_add_le_add_limsup), [EReal.limsup_add_liminf_le_limsup_add](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/EReal.html#EReal.limsup_add_liminf_le_limsup_add), [EReal.liminf_add_le_limsup_add_liminf](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/EReal.html#EReal.liminf_add_le_limsup_add_liminf) to bring them in line with similar lemmas in `Real`/`ENNReal` (see e.g. [ENNReal.limsup_mul_le](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/ENNReal.html#ENNReal.limsup_mul_le))
- removes [EReal.le_of_forall_lt_iff_le](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/EReal.html#EReal.le_of_forall_lt_iff_le), [EReal.ge_of_forall_gt_iff_ge](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/EReal.html#EReal.ge_of_forall_gt_iff_ge), [EReal.limsup_le_iff](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/EReal.html#EReal.limsup_le_iff) which were very specialized lemmas used only in the older version of the proofs above.

Author: D-Thomine

Mathlib/Data/Real/EReal.lean

@@ -923,10 +923,16 @@ def negOrderIso : EReal ≃o ERealᵒᵈ :=
     invFun := fun x => -OrderDual.ofDual x
     map_rel_iff' := neg_le_neg_iff }
 
-theorem neg_lt_iff_neg_lt {a b : EReal} : -a < b ↔ -b < a := by
+theorem neg_lt_comm {a b : EReal} : -a < b ↔ -b < a := by rw [← neg_lt_neg_iff, neg_neg]
+
+@[deprecated (since := "2024-11-19")] alias neg_lt_iff_neg_lt := neg_lt_comm
+
+theorem neg_lt_of_neg_lt {a b : EReal} (h : -a < b) : -b < a := neg_lt_comm.1 h
+
+theorem lt_neg_comm {a b : EReal} : a < -b ↔ b < -a := by
   rw [← neg_lt_neg_iff, neg_neg]
 
-theorem neg_lt_of_neg_lt {a b : EReal} (h : -a < b) : -b < a := neg_lt_iff_neg_lt.1 h
+theorem lt_neg_of_lt_neg {a b : EReal} (h : a < -b) : b < -a := lt_neg_comm.1 h
 
 lemma neg_add {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊤) (h2 : x ≠ ⊤ ∨ y ≠ ⊥) :
     - (x + y) = - x - y := by
@@ -937,64 +943,6 @@ 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
 
-/-! ### Addition and order -/
-
-lemma le_of_forall_lt_iff_le {x y : EReal} : (∀ z : ℝ, x < z → y ≤ z) ↔ y ≤ x := by
-  refine ⟨fun h ↦ WithBot.le_of_forall_lt_iff_le.1 ?_, fun h _ x_z ↦ h.trans x_z.le⟩
-  rw [WithTop.forall]
-  aesop
-
-lemma ge_of_forall_gt_iff_ge {x y : EReal} : (∀ z : ℝ, z < y → z ≤ x) ↔ y ≤ x := by
-  refine ⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩
-  rw [WithTop.forall]
-  aesop
-
-/-- This lemma is superseded by `add_le_of_forall_add_le`. -/
-private lemma top_add_le_of_forall_add_le {a b : EReal} (h : ∀ c < ⊤, ∀ d < a, c + d ≤ b) :
-    ⊤ + a ≤ b := by
-  induction a with
-  | h_bot => exact add_bot ⊤ ▸ bot_le
-  | h_real a =>
-    refine top_add_coe a ▸ le_of_forall_lt_iff_le.1 fun c b_c ↦ ?_
-    specialize h (c - a + 1) (coe_lt_top (c - a + 1)) (a - 1)
-    rw [← coe_one, ← coe_sub, ← coe_sub, ← coe_add, ← coe_add, add_add_sub_cancel, sub_add_cancel,
-      EReal.coe_lt_coe_iff] at h
-    exact (not_le_of_lt b_c (h (sub_one_lt a))).rec
-  | h_top =>
-    refine top_add_top ▸ le_of_forall_lt_iff_le.1 fun c b_c ↦ ?_
-    specialize h c (coe_lt_top c) 0 zero_lt_top
-    rw [add_zero] at h
-    exact (not_le_of_lt b_c h).rec
-
-lemma add_le_of_forall_add_le {a b c : EReal} (h : ∀ d < a, ∀ e < b, d + e ≤ c) : a + b ≤ c := by
-  induction a with
-  | h_bot => exact bot_add b ▸ bot_le
-  | h_real a => induction b with
-    | h_bot => exact add_bot (a : EReal) ▸ bot_le
-    | h_real b =>
-      refine (@ge_of_forall_gt_iff_ge c (a+b)).1 fun d d_ab ↦ ?_
-      rw [← coe_add, EReal.coe_lt_coe_iff] at d_ab
-      rcases exists_between d_ab with ⟨e, e_d, e_ab⟩
-      have key₁ : (a + d - e : ℝ) < (a : EReal) := by apply EReal.coe_lt_coe_iff.2; linarith
-      have key₂ : (e - a : ℝ) < (b : EReal) := by apply EReal.coe_lt_coe_iff.2; linarith
-      apply le_of_eq_of_le _ (h (a + d - e) key₁ (e - a) key₂)
-      rw [← coe_add, ← coe_sub,  ← coe_sub, ← coe_add, sub_add_sub_cancel, add_sub_cancel_left]
-    | h_top =>
-      rw [add_comm (a : EReal) ⊤]
-      exact top_add_le_of_forall_add_le fun d d_top e e_a ↦ (add_comm d e ▸ h e e_a d d_top)
-  | h_top => exact top_add_le_of_forall_add_le h
-
-lemma le_add_of_forall_le_add {a b c : EReal} (h₁ : a ≠ ⊥ ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ ⊥)
-    (h : ∀ d > a, ∀ e > b, c ≤ d + e) :
-    c ≤ a + b := by
-  rw [← neg_le_neg_iff, neg_add h₁ h₂]
-  refine add_le_of_forall_add_le fun d d_a e e_b ↦ ?_
-  have h₃ : d ≠ ⊥ ∨ e ≠ ⊤ := Or.inr (ne_top_of_lt e_b)
-  have h₄ : d ≠ ⊤ ∨ e ≠ ⊥ := Or.inl (ne_top_of_lt d_a)
-  rw [← neg_neg d, neg_lt_iff_neg_lt, neg_neg a] at d_a
-  rw [← neg_neg e, neg_lt_iff_neg_lt, neg_neg b] at e_b
-  exact le_neg_of_le_neg <| neg_add h₃ h₄ ▸ h (- d) d_a (- e) e_b
-
 /-!
 ### Subtraction
 
@@ -1023,6 +971,12 @@ theorem top_sub_coe (x : ℝ) : (⊤ : EReal) - x = ⊤ :=
 theorem coe_sub_bot (x : ℝ) : (x : EReal) - ⊥ = ⊤ :=
   rfl
 
+lemma sub_bot {a : EReal} (h : a ≠ ⊥) : a - ⊥ = ⊤ := by
+  induction a
+  · simp only [ne_eq, not_true_eq_false] at h
+  · rw [coe_sub_bot]
+  · rw [top_sub_bot]
+
 theorem sub_le_sub {x y z t : EReal} (h : x ≤ y) (h' : t ≤ z) : x - z ≤ y - t :=
   add_le_add h (neg_le_neg_iff.2 h')
 
@@ -1047,11 +1001,105 @@ theorem toReal_sub {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠
   lift y to ℝ using ⟨hy, h'y⟩
   rfl
 
-lemma add_sub_cancel_right {a : EReal} {b : Real} : a + b - b = a := by
+lemma sub_add_cancel_left {a : EReal} {b : Real} : a - b + b = a := by
   induction a
-  · rw [bot_add b, bot_sub b]
+  · rw [bot_sub b, bot_add b]
   · norm_cast; linarith
-  · rw [top_add_of_ne_bot (coe_ne_bot b), top_sub_coe]
+  · rw [top_sub_coe b, top_add_coe b]
+
+lemma add_sub_cancel_right {a : EReal} {b : Real} : a + b - b = a := by
+  rw [sub_eq_add_neg, add_assoc, add_comm (b : EReal), ← add_assoc, ← sub_eq_add_neg]
+  exact sub_add_cancel_left
+
+lemma le_sub_iff_add_le {a b c : EReal} (hb : b ≠ ⊥ ∨ c ≠ ⊥) (ht : b ≠ ⊤ ∨ c ≠ ⊤) :
+    a ≤ c - b ↔ a + b ≤ c := by
+  induction b with
+  | h_bot =>
+    simp only [ne_eq, not_true_eq_false, false_or] at hb
+    simp only [sub_bot hb, le_top, add_bot, bot_le]
+  | h_real b =>
+    rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel_left]
+  | h_top =>
+    simp only [ne_eq, not_true_eq_false, false_or, sub_top, le_bot_iff] at ht ⊢
+    refine ⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩
+    by_contra ha
+    exact (h.trans_lt (Ne.lt_top ht)).ne (add_top_iff_ne_bot.2 ha)
+
+lemma sub_le_iff_le_add {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) :
+    a - b ≤ c ↔ a ≤ c + b := by
+  suffices a + (-b) ≤ c ↔ a ≤ c - (-b) by simpa [sub_eq_add_neg]
+  refine (le_sub_iff_add_le ?_ ?_).symm <;> simpa
+
+protected theorem lt_sub_iff_add_lt {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) :
+    c < a - b ↔ c + b < a :=
+  lt_iff_lt_of_le_iff_le (sub_le_iff_le_add h₁ h₂)
+
+theorem sub_le_of_le_add {a b c : EReal} (h : a ≤ b + c) : a - c ≤ b := by
+  induction c with
+  | h_bot => rw [add_bot, le_bot_iff] at h; simp only [h, bot_sub, bot_le]
+  | h_real c => exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h
+  | h_top => simp only [sub_top, bot_le]
+
+/-- See also `EReal.sub_le_of_le_add`.-/
+theorem sub_le_of_le_add' {a b c : EReal} (h : a ≤ b + c) : a - b ≤ c :=
+  sub_le_of_le_add (add_comm b c ▸ h)
+
+lemma add_le_of_le_sub {a b c : EReal} (h : a ≤ b - c) : a + c ≤ b := by
+  rw [← neg_neg c]
+  exact sub_le_of_le_add h
+
+lemma sub_lt_iff {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊥) (h₂ : b ≠ ⊤ ∨ c ≠ ⊤) :
+    c - b < a ↔ c < a + b :=
+  lt_iff_lt_of_le_iff_le (le_sub_iff_add_le h₁ h₂)
+
+lemma add_lt_of_lt_sub {a b c : EReal} (h : a < b - c) : a + c < b := by
+  contrapose! h
+  exact sub_le_of_le_add h
+
+lemma sub_lt_of_lt_add {a b c : EReal} (h : a < b + c) : a - c < b :=
+  add_lt_of_lt_sub <| by rwa [sub_eq_add_neg, neg_neg]
+
+/-- See also `EReal.sub_lt_of_lt_add`.-/
+lemma sub_lt_of_lt_add' {a b c : EReal} (h : a < b + c) : a - b < c :=
+  sub_lt_of_lt_add <| by rwa [add_comm]
+
+/-! ### Addition and order -/
+
+lemma le_of_forall_lt_iff_le {x y : EReal} : (∀ z : ℝ, x < z → y ≤ z) ↔ y ≤ x := by
+  refine ⟨fun h ↦ WithBot.le_of_forall_lt_iff_le.1 ?_, fun h _ x_z ↦ h.trans x_z.le⟩
+  rw [WithTop.forall]
+  aesop
+
+lemma ge_of_forall_gt_iff_ge {x y : EReal} : (∀ z : ℝ, z < y → z ≤ x) ↔ y ≤ x := by
+  refine ⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩
+  rw [WithTop.forall]
+  aesop
+
+private lemma exists_lt_add_left {a b c : EReal} (hc : c < a + b) : ∃ a' < a, c < a' + b := by
+  obtain ⟨a', hc', ha'⟩ := exists_between (sub_lt_of_lt_add hc)
+  refine ⟨a', ha', (sub_lt_iff (.inl ?_) (.inr hc.ne_top)).1 hc'⟩
+  contrapose! hc
+  exact hc ▸ (add_bot a).symm ▸ bot_le
+
+private lemma exists_lt_add_right {a b c : EReal} (hc : c < a + b) : ∃ b' < b, c < a + b' := by
+  simp_rw [add_comm a] at hc ⊢; exact exists_lt_add_left hc
+
+lemma add_le_of_forall_lt {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) : a + b ≤ c := by
+  refine le_of_forall_ge_of_dense fun d hd ↦ ?_
+  obtain ⟨a', ha', hd⟩ := exists_lt_add_left hd
+  obtain ⟨b', hb', hd⟩ := exists_lt_add_right hd
+  exact hd.le.trans (h _ ha' _ hb')
+
+lemma le_add_of_forall_gt {a b c : EReal} (h₁ : a ≠ ⊥ ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ ⊥)
+    (h : ∀ a' > a, ∀ b' > b, c ≤ a' + b') : c ≤ a + b := by
+  rw [← neg_le_neg_iff, neg_add h₁ h₂]
+  exact add_le_of_forall_lt fun a' ha' b' hb' ↦ le_neg_of_le_neg
+    <| (h (-a') (lt_neg_of_lt_neg ha') (-b') (lt_neg_of_lt_neg hb')).trans_eq
+    (neg_add (.inr hb'.ne_top) (.inl ha'.ne_top)).symm
+
+@[deprecated (since := "2024-11-19")] alias top_add_le_of_forall_add_le := add_le_of_forall_lt
+@[deprecated (since := "2024-11-19")] alias add_le_of_forall_add_le := add_le_of_forall_lt
+@[deprecated (since := "2024-11-19")] alias le_add_of_forall_le_add := le_add_of_forall_gt
 
 lemma _root_.ENNReal.toEReal_sub {x y : ℝ≥0∞} (hy_top : y ≠ ∞) (h_le : y ≤ x) :
     (x - y).toEReal = x.toEReal - y.toEReal := by
@@ -1576,7 +1624,7 @@ lemma div_right_distrib_of_nonneg {a b c : EReal} (h : 0 ≤ a) (h' : 0 ≤ b) :
     (a + b) / c = (a / c) + (b / c) :=
   EReal.right_distrib_of_nonneg h h'
 
-/-! #### Division and Order s -/
+/-! #### Division and Order -/
 
 lemma monotone_div_right_of_nonneg {b : EReal} (h : 0 ≤ b) : Monotone fun a ↦ a / b :=
   fun _ _ h' ↦ mul_le_mul_of_nonneg_right h' (inv_nonneg_of_nonneg h)

Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean

@@ -483,7 +483,7 @@ lemma coverEntropyEntourage_le_log_coverMincard_div {T : X → X} {F : Set X} (F
     eventually_atTop.2 ⟨1, fun m m_pos ↦ log_coverMincard_le_add F_inv U_symm n_pos m_pos⟩
   apply ((limsup_le_limsup) key).trans
   suffices h : atTop.limsup v = 0 by
-    have := @limsup_add_le_add_limsup ℕ atTop u v
+    have := @limsup_add_le ℕ atTop u v
     rw [h, add_zero] at this
     specialize this (Or.inr EReal.zero_ne_top) (Or.inr EReal.zero_ne_bot)
     exact this.trans_eq (limsup_const (log (coverMincard T F U n) / n))

Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean

@@ -527,7 +527,7 @@ theorem exists_upperSemicontinuous_lt_integral_gt [SigmaFinite μ] (f : α → 
   rcases exists_lt_lowerSemicontinuous_integral_lt (fun x => -f x) hf.neg εpos with
     ⟨g, g_lt_f, gcont, g_integrable, g_lt_top, gint⟩
   refine ⟨fun x => -g x, ?_, ?_, ?_, ?_, ?_⟩
-  · exact fun x => EReal.neg_lt_iff_neg_lt.1 (by simpa only [EReal.coe_neg] using g_lt_f x)
+  · exact fun x => EReal.neg_lt_comm.1 (by simpa only [EReal.coe_neg] using g_lt_f x)
   · exact
       continuous_neg.comp_lowerSemicontinuous_antitone gcont fun x y hxy =>
         EReal.neg_le_neg_iff.2 hxy

Mathlib/Topology/Instances/EReal.lean

@@ -214,65 +214,56 @@ lemma liminf_neg : liminf (- v) f = - limsup v f :=
 lemma limsup_neg : limsup (- v) f = - liminf v f :=
   EReal.negOrderIso.liminf_apply.symm
 
-lemma add_liminf_le_liminf_add : (liminf u f) + (liminf v f) ≤ liminf (u + v) f := by
-  refine add_le_of_forall_add_le fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
+lemma le_liminf_add : (liminf u f) + (liminf v f) ≤ liminf (u + v) f := by
+  refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
   filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
-  exact lt_trans c_ab (add_lt_add a_x b_x)
+  exact c_ab.trans (add_lt_add a_x b_x)
 
-lemma limsup_add_le_add_limsup (h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤)
-    (h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥) :
+lemma limsup_add_le (h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤) (h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥) :
     limsup (u + v) f ≤ (limsup u f) + (limsup v f) := by
-  refine le_add_of_forall_le_add h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
+  refine le_add_of_forall_gt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
   filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x
   exact (add_lt_add a_x b_x).trans c_ab
 
-lemma limsup_add_liminf_le_limsup_add : (limsup u f) + (liminf v f) ≤ limsup (u + v) f :=
-  add_le_of_forall_add_le fun _ a_u _ b_v ↦ (le_limsup_iff).2 fun _ c_ab ↦
-    Frequently.mono (Frequently.and_eventually ((frequently_lt_of_lt_limsup) a_u)
-    ((eventually_lt_of_lt_liminf) b_v)) fun _ ab_x ↦ c_ab.trans (add_lt_add ab_x.1 ab_x.2)
+lemma le_limsup_add : (limsup u f) + (liminf v f) ≤ limsup (u + v) f :=
+  add_le_of_forall_lt fun _ a_u _ b_v ↦ (le_limsup_iff).2 fun _ c_ab ↦
+    (((frequently_lt_of_lt_limsup) a_u).and_eventually ((eventually_lt_of_lt_liminf) b_v)).mono
+    fun _ ab_x ↦ c_ab.trans (add_lt_add ab_x.1 ab_x.2)
 
-lemma liminf_add_le_limsup_add_liminf (h : limsup u f ≠ ⊥ ∨ liminf v f ≠ ⊤)
-    (h' : limsup u f ≠ ⊤ ∨ liminf v f ≠ ⊥) :
+lemma liminf_add_le (h : limsup u f ≠ ⊥ ∨ liminf v f ≠ ⊤) (h' : limsup u f ≠ ⊤ ∨ liminf v f ≠ ⊥) :
     liminf (u + v) f ≤ (limsup u f) + (liminf v f) :=
-  le_add_of_forall_le_add h h' fun _ a_u _ b_v ↦ (liminf_le_iff).2 fun _ c_ab ↦
-    Frequently.mono (Frequently.and_eventually ((frequently_lt_of_liminf_lt) b_v)
-    ((eventually_lt_of_limsup_lt) a_u)) fun _ ab_x ↦ (add_lt_add ab_x.2 ab_x.1).trans c_ab
+  le_add_of_forall_gt h h' fun _ a_u _ b_v ↦ (liminf_le_iff).2 fun _ c_ab ↦
+    (((frequently_lt_of_liminf_lt) b_v).and_eventually ((eventually_lt_of_limsup_lt) a_u)).mono
+    fun _ ab_x ↦ (add_lt_add ab_x.2 ab_x.1).trans c_ab
+
+@[deprecated (since := "2024-11-11")] alias add_liminf_le_liminf_add := le_liminf_add
+@[deprecated (since := "2024-11-11")] alias limsup_add_le_add_limsup := limsup_add_le
+@[deprecated (since := "2024-11-11")] alias limsup_add_liminf_le_limsup_add := le_limsup_add
+@[deprecated (since := "2024-11-11")] alias liminf_add_le_limsup_add_liminf := liminf_add_le
 
 variable {a b : EReal}
 
 lemma limsup_add_bot_of_ne_top (h : limsup u f = ⊥) (h' : limsup v f ≠ ⊤) :
     limsup (u + v) f = ⊥ := by
-  apply le_bot_iff.1 (le_trans (limsup_add_le_add_limsup (Or.inr h') _) _)
-  · rw [h]; exact Or.inl bot_ne_top
+  apply le_bot_iff.1 ((limsup_add_le (.inr h') _).trans _)
+  · rw [h]; exact .inl bot_ne_top
   · rw [h, bot_add]
 
 lemma limsup_add_le_of_le (ha : limsup u f < a) (hb : limsup v f ≤ b) :
     limsup (u + v) f ≤ a + b := by
-  rcases eq_top_or_lt_top b with (rfl | h)
+  rcases eq_top_or_lt_top b with rfl | h
   · rw [add_top_of_ne_bot ha.ne_bot]; exact le_top
-  · exact le_trans (limsup_add_le_add_limsup (Or.inr (lt_of_le_of_lt hb h).ne) (Or.inl ha.ne_top))
-      (add_le_add ha.le hb)
+  · exact (limsup_add_le (.inr (hb.trans_lt h).ne) (.inl ha.ne_top)).trans (add_le_add ha.le hb)
 
 lemma liminf_add_gt_of_gt (ha : a < liminf u f) (hb : b < liminf v f) :
     a + b < liminf (u + v) f :=
-  lt_of_lt_of_le (add_lt_add ha hb) add_liminf_le_liminf_add
+  (add_lt_add ha hb).trans_le le_liminf_add
 
 lemma liminf_add_top_of_ne_bot (h : liminf u f = ⊤) (h' : liminf v f ≠ ⊥) :
     liminf (u + v) f = ⊤ := by
-  apply top_le_iff.1 (le_trans _ (add_liminf_le_liminf_add))
+  apply top_le_iff.1 (le_trans _ le_liminf_add)
   rw [h, top_add_of_ne_bot h']
 
-lemma limsup_le_iff {b : EReal} : limsup u f ≤ b ↔ ∀ c : ℝ, b < c → ∀ᶠ a : α in f, u a ≤ c := by
-  rw [← le_of_forall_lt_iff_le]
-  refine ⟨?_, ?_⟩ <;> intro h c b_c
-  · rcases exists_between_coe_real b_c with ⟨d, b_d, d_c⟩
-    apply mem_of_superset (eventually_lt_of_limsup_lt (lt_of_le_of_lt (h d b_d) d_c))
-    rw [Set.setOf_subset_setOf]
-    exact fun _ h' ↦ h'.le
-  · rcases eq_or_neBot f with rfl | _
-    · simp only [limsup_bot, bot_le]
-    · exact (limsup_le_of_le) (h c b_c)
-
 end LimInfSup
 
 /-! ### Continuity of addition -/