feat: push lemmas for Filter.NeBot (#35261)

Author: j-loreaux

Mathlib/Order/Filter/Basic.lean

@@ -249,7 +249,8 @@ end CompleteLattice
 
 theorem NeBot.ne {f : Filter α} (hf : NeBot f) : f ≠ ⊥ := hf.ne'
 
-@[simp] theorem not_neBot {f : Filter α} : ¬f.NeBot ↔ f = ⊥ := neBot_iff.not_left
+@[simp, push]
+theorem not_neBot {f : Filter α} : ¬f.NeBot ↔ f = ⊥ := neBot_iff.not_left
 
 theorem NeBot.mono {f g : Filter α} (hf : NeBot f) (hg : f ≤ g) : NeBot g :=
   ⟨ne_bot_of_le_ne_bot hf.1 hg⟩

Mathlib/Order/Filter/Defs.lean

@@ -271,6 +271,7 @@ class NeBot (f : Filter α) : Prop where
   /-- The filter is nontrivial: `f ≠ ⊥` or equivalently, `∅ ∉ f`. -/
   ne' : f ≠ ⊥
 
+@[push ←]
 theorem neBot_iff {f : Filter α} : NeBot f ↔ f ≠ ⊥ :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 

Mathlib/Topology/Algebra/InfiniteSum/Defs.lean

@@ -162,7 +162,7 @@ notation3 "∑' "(...)", "r:67:(scoped f => tsum f (unconditional _)) => r
 @[to_additive]
 lemma hasProd_bot (hL : ¬L.NeBot) (f : β → α) (a : α) :
     HasProd f a L := by
-  have : L.filter = ⊥ := by contrapose! hL; exact ⟨⟨hL⟩⟩
+  have : L.filter = ⊥ := by contrapose! hL; exact ⟨hL⟩
   rw [HasProd, this]
   exact tendsto_bot
 

Mathlib/Topology/Algebra/InfiniteSum/SummationFilter.lean

@@ -133,11 +133,10 @@ for the intended applications, and this avoids requiring a `DecidableEq` instanc
 /-- If `L` has well-defined support, then so does its map along an embedding. -/
 instance (L : SummationFilter β) [HasSupport L] (f : β ↪ γ) : HasSupport (L.map f) := by
   constructor
-  by_cases h : L.NeBot
+  obtain (h | h) := L.neBot_or_eq_bot
   · simp only [map_filter, eventually_map, Finset.coe_map, image_subset_iff, support_map]
     filter_upwards [L.eventually_le_support] with a using by grind
-  · have : L.filter = ⊥ := by contrapose! h; exact ⟨⟨h⟩⟩
-    simp [this]
+  · simp [h]
 
 /-- Pullback of a summation filter along an embedding. -/
 @[simps] noncomputable def comap (L : SummationFilter β) (f : γ ↪ β) : SummationFilter γ where