feat: add Filter.eq_or_neBot (#5230)

Also add `Filter.limsup_bot`, `Filter.liminf_bot`, and golf some proofs using new lemmas.

Mathlib/Analysis/Complex/LocallyUniformLimit.lean

@@ -99,9 +99,8 @@ theorem norm_cderiv_sub_lt (hr : 0 < r) (hfg : ∀ w ∈ sphere z r, ‖f w - g
 theorem _root_.TendstoUniformlyOn.cderiv (hF : TendstoUniformlyOn F f φ (cthickening δ K))
     (hδ : 0 < δ) (hFn : ∀ᶠ n in φ, ContinuousOn (F n) (cthickening δ K)) :
     TendstoUniformlyOn (cderiv δ ∘ F) (cderiv δ f) φ K := by
-  by_cases φ = ⊥
-  · simp only [h, TendstoUniformlyOn, eventually_bot, imp_true_iff]
-  haveI : φ.NeBot := neBot_iff.2 h
+  rcases φ.eq_or_neBot with rfl | hne
+  · simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
   have e1 : ContinuousOn f (cthickening δ K) := TendstoUniformlyOn.continuousOn hF hFn
   rw [tendstoUniformlyOn_iff] at hF ⊢
   rintro ε hε
@@ -167,9 +166,8 @@ theorem _root_.TendstoLocallyUniformlyOn.deriv (hf : TendstoLocallyUniformlyOn F
     (hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) :
     TendstoLocallyUniformlyOn (deriv ∘ F) (deriv f) φ U := by
   rw [tendstoLocallyUniformlyOn_iff_forall_isCompact hU]
-  by_cases φ = ⊥
-  · simp only [h, TendstoUniformlyOn, eventually_bot, imp_true_iff]
-  haveI : φ.NeBot := neBot_iff.2 h
+  rcases φ.eq_or_neBot with rfl | hne
+  · simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
   rintro K hKU hK
   obtain ⟨δ, hδ, hK4, h⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
   refine' h.congr_right fun z hz => cderiv_eq_deriv hU (hf.differentiableOn hF hU) hδ _

Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

@@ -153,9 +153,8 @@ theorem measurable_limit_of_tendsto_metrizable_ae {ι} [Countable ι] [Nonempty
     ∃ (f_lim : α → β) (hf_lim_meas : Measurable f_lim),
       ∀ᵐ x ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x)) := by
   inhabit ι
-  rcases eq_or_ne L ⊥ with (rfl | hL)
+  rcases eq_or_neBot L with (rfl | hL)
   · exact ⟨(hf default).mk _, (hf default).measurable_mk, eventually_of_forall fun x => tendsto_bot⟩
-  haveI : NeBot L := ⟨hL⟩
   let p : α → (ι → β) → Prop := fun x f' => ∃ l : β, Tendsto (fun n => f' n) L (𝓝 l)
   have hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x := fun x hx =>
     aeSeq.fun_prop_of_mem_aeSeqSet hf hx

Mathlib/MeasureTheory/Constructions/Polish.lean

@@ -820,10 +820,8 @@ theorem isClopenable_iff_measurableSet : IsClopenable s ↔ MeasurableSet s := b
 theorem measurableSet_exists_tendsto [hγ : OpensMeasurableSpace γ] [Countable ι] {l : Filter ι}
     [l.IsCountablyGenerated] {f : ι → β → γ} (hf : ∀ i, Measurable (f i)) :
     MeasurableSet { x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c) } := by
-  by_cases hl : l.NeBot
-  swap;
-  · rw [not_neBot] at hl
-    simp [hl]
+  rcases l.eq_or_neBot with rfl | hl
+  · simp
   letI := upgradePolishSpace γ
   rcases l.exists_antitone_basis with ⟨u, hu⟩
   simp_rw [← cauchy_map_iff_exists_tendsto]

Mathlib/MeasureTheory/Covering/DensityTheorem.lean

@@ -118,8 +118,8 @@ theorem tendsto_closedBall_filterAt {K : ℝ} {x : α} {ι : Type _} {l : Filter
   refine' (vitaliFamily μ K).tendsto_filterAt_iff.mpr ⟨_, fun ε hε => _⟩
   · filter_upwards [xmem, δlim self_mem_nhdsWithin] with j hj h'j
     exact closedBall_mem_vitaliFamily_of_dist_le_mul μ hj h'j
-  · by_cases l.NeBot
-    swap; · simp [not_neBot.1 h]
+  · rcases l.eq_or_neBot with rfl | h
+    · simp
     have hK : 0 ≤ K := by
       rcases (xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩
       have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩

Mathlib/MeasureTheory/Measure/Portmanteau.lean

@@ -102,17 +102,14 @@ Either of these will later be shown to be equivalent to the weak convergence of
 of measures.
 -/
 
-
 variable {Ω : Type _} [MeasurableSpace Ω]
 
 theorem le_measure_compl_liminf_of_limsup_measure_le {ι : Type _} {L : Filter ι} {μ : Measure Ω}
     {μs : ι → Measure Ω} [IsProbabilityMeasure μ] [∀ i, IsProbabilityMeasure (μs i)] {E : Set Ω}
     (E_mble : MeasurableSet E) (h : (L.limsup fun i => μs i E) ≤ μ E) :
     μ (Eᶜ) ≤ L.liminf fun i => μs i (Eᶜ) := by
-  by_cases L_bot : L = ⊥
-  · simp only [L_bot, le_top,
-      show liminf (fun i => μs i (Eᶜ)) ⊥ = ⊤ by simp only [liminf, Filter.map_bot, limsInf_bot]]
-  have : L.NeBot := { ne' := L_bot }
+  rcases L.eq_or_neBot with rfl | hne
+  · simp only [liminf_bot, le_top]
   have meas_Ec : μ (Eᶜ) = 1 - μ E := by
     simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne
   have meas_i_Ec : ∀ i, μs i (Eᶜ) = 1 - μs i E := by
@@ -139,10 +136,8 @@ theorem limsup_measure_compl_le_of_le_liminf_measure {ι : Type _} {L : Filter 
     {μs : ι → Measure Ω} [IsProbabilityMeasure μ] [∀ i, IsProbabilityMeasure (μs i)] {E : Set Ω}
     (E_mble : MeasurableSet E) (h : μ E ≤ L.liminf fun i => μs i E) :
     (L.limsup fun i => μs i (Eᶜ)) ≤ μ (Eᶜ) := by
-  by_cases L_bot : L = ⊥
-  · simp only [L_bot, bot_le,
-      show limsup (fun i => μs i (Eᶜ)) ⊥ = ⊥ by simp only [limsup, Filter.map_bot, limsSup_bot]]
-  have : L.NeBot := { ne' := L_bot }
+  rcases L.eq_or_neBot with rfl | hne
+  · simp only [limsup_bot, bot_le]
   have meas_Ec : μ (Eᶜ) = 1 - μ E := by
     simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne
   have meas_i_Ec : ∀ i, μs i (Eᶜ) = 1 - μs i E := by
@@ -341,8 +336,8 @@ theorem FiniteMeasure.limsup_measure_closed_le_of_tendsto {Ω ι : Type _} {L :
     [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] {μ : FiniteMeasure Ω}
     {μs : ι → FiniteMeasure Ω} (μs_lim : Tendsto μs L (𝓝 μ)) {F : Set Ω} (F_closed : IsClosed F) :
     (L.limsup fun i => (μs i : Measure Ω) F) ≤ (μ : Measure Ω) F := by
-  by_cases L = ⊥
-  · simp only [h, limsup, Filter.map_bot, limsSup_bot, ENNReal.bot_eq_zero, zero_le]
+  rcases L.eq_or_neBot with rfl | hne
+  · simp only [limsup_bot, bot_le]
   apply ENNReal.le_of_forall_pos_le_add
   intro ε ε_pos _
   let δs := fun n : ℕ => (1 : ℝ) / (n + 1)
@@ -367,7 +362,6 @@ theorem FiniteMeasure.limsup_measure_closed_le_of_tendsto {Ω ι : Type _} {L :
   have ev_near' := Eventually.mono ev_near fun n => le_trans
     (measure_le_lintegral_thickenedIndicator (μs n : Measure Ω) F_closed.measurableSet (δs_pos M))
   apply (Filter.limsup_le_limsup ev_near').trans
-  have : NeBot L := ⟨h⟩
   rw [limsup_const]
   apply le_trans (add_le_add (hM M rfl.le).le (le_refl (ε / 2 : ℝ≥0∞)))
   simp only [add_assoc, ENNReal.add_halves, le_refl]

Mathlib/Order/Filter/Basic.lean

@@ -519,6 +519,10 @@ theorem not_disjoint_self_iff : ¬Disjoint f f ↔ f.NeBot := by rw [disjoint_se
 theorem bot_sets_eq : (⊥ : Filter α).sets = univ := rfl
 #align filter.bot_sets_eq Filter.bot_sets_eq
 
+/-- Either `f = ⊥` or `Filter.NeBot f`. This is a version of `eq_or_ne` that uses `Filter.NeBot`
+as the second alternative, to be used as an instance. -/
+theorem eq_or_neBot (f : Filter α) : f = ⊥ ∨ NeBot f := (eq_or_ne f ⊥).imp_right NeBot.mk
+
 theorem sup_sets_eq {f g : Filter α} : (f ⊔ g).sets = f.sets ∩ g.sets :=
   (giGenerate α).gc.u_inf
 #align filter.sup_sets_eq Filter.sup_sets_eq

Mathlib/Order/LiminfLimsup.lean

@@ -618,12 +618,16 @@ theorem limsSup_bot : limsSup (⊥ : Filter α) = ⊥ :=
 set_option linter.uppercaseLean3 false in
 #align filter.Limsup_bot Filter.limsSup_bot
 
+@[simp] theorem limsup_bot (f : β → α) : limsup f ⊥ = ⊥ := by simp [limsup]
+
 @[simp]
 theorem limsInf_bot : limsInf (⊥ : Filter α) = ⊤ :=
   top_unique <| le_sSup <| by simp
 set_option linter.uppercaseLean3 false in
 #align filter.Liminf_bot Filter.limsInf_bot
 
+@[simp] theorem liminf_bot (f : β → α) : liminf f ⊥ = ⊤ := by simp [liminf]
+
 @[simp]
 theorem limsSup_top : limsSup (⊤ : Filter α) = ⊤ :=
   top_unique <| le_sInf <| by simp [eq_univ_iff_forall]; exact fun b hb => top_unique <| hb _

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

@@ -236,10 +236,8 @@ theorem tendsto_of_no_upcrossings [DenselyOrdered α] {f : Filter β} {u : β 
     (h : f.IsBoundedUnder (· ≤ ·) u := by isBoundedDefault)
     (h' : f.IsBoundedUnder (· ≥ ·) u := by isBoundedDefault) :
     ∃ c : α, Tendsto u f (𝓝 c) := by
-  by_cases hbot : f = ⊥;
-  · rw [hbot]
-    exact ⟨sInf ∅, tendsto_bot⟩
-  haveI : NeBot f := ⟨hbot⟩
+  rcases f.eq_or_neBot with rfl | hbot
+  · exact ⟨sInf ∅, tendsto_bot⟩
   refine' ⟨limsup u f, _⟩
   apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h'
   by_contra' hlt