feat(Order/Filter): add Filter.tendsto_image_smallSets (#8811)

- Add `Filter.tendsto_image_smallSets` and
  `Filter.Tendsto.image_smallSets`.
- Generalize `Filter.eventually_all` from `Type*` to `Sort*`.
- Protect `Filter.HasBasis.smallSets`.
- Fix a porting note about `Filter.eventually_smallSets`:
  the Lean 3 proof works in Lean 4 now.

Mathlib/Order/Filter/Basic.lean

@@ -1164,9 +1164,8 @@ theorem eventually_congr {f : Filter α} {p q : α → Prop} (h : ∀ᶠ x in f,
 #align filter.eventually_congr Filter.eventually_congr
 
 @[simp]
-theorem eventually_all {ι : Type*} [Finite ι] {l} {p : ι → α → Prop} :
+theorem eventually_all {ι : Sort*} [Finite ι] {l} {p : ι → α → Prop} :
     (∀ᶠ x in l, ∀ i, p i x) ↔ ∀ i, ∀ᶠ x in l, p i x := by
-  cases nonempty_fintype ι
   simpa only [Filter.Eventually, setOf_forall] using iInter_mem
 #align filter.eventually_all Filter.eventually_all
 
@@ -1203,10 +1202,9 @@ theorem eventually_or_distrib_right {f : Filter α} {p : α → Prop} {q : Prop}
   simp only [@or_comm _ q, eventually_or_distrib_left]
 #align filter.eventually_or_distrib_right Filter.eventually_or_distrib_right
 
-@[simp]
 theorem eventually_imp_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
-    (∀ᶠ x in f, p → q x) ↔ p → ∀ᶠ x in f, q x := by
-  simp only [imp_iff_not_or, eventually_or_distrib_left]
+    (∀ᶠ x in f, p → q x) ↔ p → ∀ᶠ x in f, q x :=
+  eventually_all
 #align filter.eventually_imp_distrib_left Filter.eventually_imp_distrib_left
 
 @[simp]

Mathlib/Order/Filter/SmallSets.lean

@@ -42,7 +42,7 @@ theorem smallSets_eq_generate {f : Filter α} : f.smallSets = generate (powerset
   rfl
 #align filter.small_sets_eq_generate Filter.smallSets_eq_generate
 
-theorem HasBasis.smallSets {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) :
+protected theorem HasBasis.smallSets {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) :
     HasBasis l.smallSets p fun i => 𝒫 s i :=
   h.lift' monotone_powerset
 #align filter.has_basis.small_sets Filter.HasBasis.smallSets
@@ -58,12 +58,9 @@ theorem tendsto_smallSets_iff {f : α → Set β} :
   (hasBasis_smallSets lb).tendsto_right_iff
 #align filter.tendsto_small_sets_iff Filter.tendsto_smallSets_iff
 
--- porting note: the proof was `eventually_lift'_iff monotone_powerset`
--- but it timeouts in Lean 4
 theorem eventually_smallSets {p : Set α → Prop} :
-    (∀ᶠ s in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t, t ⊆ s → p t := by
-  rw [smallSets, eventually_lift'_iff]; rfl
-  exact monotone_powerset
+    (∀ᶠ s in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t, t ⊆ s → p t :=
+  eventually_lift'_iff monotone_powerset
 #align filter.eventually_small_sets Filter.eventually_smallSets
 
 theorem eventually_smallSets' {p : Set α → Prop} (hp : ∀ ⦃s t⦄, s ⊆ t → p t → p s) :
@@ -81,6 +78,16 @@ theorem frequently_smallSets_mem (l : Filter α) : ∃ᶠ s in l.smallSets, s 
   frequently_smallSets.2 fun t ht => ⟨t, Subset.rfl, ht⟩
 #align filter.frequently_small_sets_mem Filter.frequently_smallSets_mem
 
+@[simp]
+lemma tendsto_image_smallSets {f : α → β} :
+    Tendsto (f '' ·) la.smallSets lb.smallSets ↔ Tendsto f la lb := by
+  rw [tendsto_smallSets_iff]
+  refine forall₂_congr fun u hu ↦ ?_
+  rw [eventually_smallSets' fun s t hst ht ↦ (image_subset _ hst).trans ht]
+  simp only [image_subset_iff, exists_mem_subset_iff, mem_map]
+
+alias ⟨_, Tendsto.image_smallSets⟩ := tendsto_image_smallSets
+
 theorem HasAntitoneBasis.tendsto_smallSets {ι} [Preorder ι] {s : ι → Set α}
     (hl : l.HasAntitoneBasis s) : Tendsto s atTop l.smallSets :=
   tendsto_smallSets_iff.2 fun _t ht => hl.eventually_subset ht