feat(Order/Filter/Pointwise): ((∀ᶠ|∃ᶠ) x in op f, p x) ↔ ((∀ᶠ|∃ᶠ) x in f, p (op x)) (leanprover-community#35312)

This lemma is required when I prove that $z \mapsto \sin^{-1} z^{-1}$ is not meromorphic at $0$:

```lean4
@[simp]
lemma Filter.frequently_inv {α : Type*} [Inv α] {f : Filter α} {p : α → Prop} :
    (∃ᶠ a in f⁻¹, p a) ↔ (∃ᶠ a in f, p a⁻¹) :=
  frequently_map

example : ¬(∀ᶠ z in 𝓝[≠] (0 : ℂ), sin⁻¹ z⁻¹ = 0) ↔ (∃ᶠ z in cobounded ℂ, sin z ≠ 0) := by
  simp [← inv_cobounded₀]
```

So I added the simp lemmas of `(∀ᶠ|∃ᶠ) x in op f, p x` for unary operations `op` (`-f`, `f⁻¹` & `a • f`).

While I was at it, I also added the simp lemmas of `∃ᶠ x in pure a, p x` & `∃ᶠ x in (0|1), p x`, which previously existed only for the `∀ᶠ` versions.

Binary operation versions will be added if necessary.

<details>
<summary>Appendix: Full proof of that $z \mapsto \sin^{-1} z^{-1}$ is not meromorphic at $0$</summary>

```lean4
module
import Mathlib.Analysis.Meromorphic.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.Analysis.SpecificLimits.RCLike

open Complex Filter Bornology
open scoped Real Topology Pointwise

@[simp]
lemma Filter.frequently_inv {α : Type*} [Inv α] {f : Filter α} {p : α → Prop} :
    (∃ᶠ a in f⁻¹, p a) ↔ (∃ᶠ a in f, p a⁻¹) :=
  frequently_map

example : ¬MeromorphicAt (fun z => sin⁻¹ z⁻¹) 0 := by
  apply mt MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
  conv => equals (∃ᶠ z in cobounded ℂ, sin z ≠ 0) ∧ (∃ᶠ z in cobounded ℂ, sin z = 0) =>
    simp [← inv_cobounded₀]
  constructor
  case left =>
    have ht : Tendsto (fun x : ℝ ↦ ↑x * I) (cobounded ℝ) (cobounded ℂ) := by
      have ht₁ : Tendsto ((↑) : ℝ → ℂ) (cobounded ℝ) (cobounded ℂ) :=
        RCLike.tendsto_ofReal_cobounded_cobounded ℂ
      have ht₂ : Tendsto (fun z : ℂ ↦ z * I) (cobounded ℂ) (cobounded ℂ) :=
        tendsto_mul_right_cobounded (by simp)
      exact ht₂.comp ht₁
    refine ht.frequently_map _ (fun x ↦ mt ?_) (eventually_ne_cobounded 0).frequently
    rw [sin_eq_zero_iff]
    rintro ⟨n, hn⟩
    simpa using congr_arg im hn
  case right =>
    suffices ht : Tendsto (fun n : ℤ ↦ (↑n * ↑π : ℂ)) atTop (cobounded ℂ) by
      apply ht.frequently; simp [sin_int_mul_pi, atTop_neBot]
    have ht₁ : Tendsto ((↑) : ℤ → ℝ) atTop (cobounded ℝ) := tendsto_intCast_atTop_cobounded
    have ht₂ : Tendsto ((↑) : ℝ → ℂ) (cobounded ℝ) (cobounded ℂ) :=
      RCLike.tendsto_ofReal_cobounded_cobounded ℂ
    have ht₃ : Tendsto (fun z : ℂ ↦ z * ↑π) (cobounded ℂ) (cobounded ℂ) :=
      tendsto_mul_right_cobounded (by simp)
    exact ht₃.comp <| ht₂.comp ht₁
```

</details>

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Author: Komyyy

Mathlib/Order/Filter/Map.lean

@@ -145,6 +145,10 @@ theorem pure_sets (a : α) : (pure a : Filter α).sets = { s | a ∈ s } :=
 theorem eventually_pure {a : α} {p : α → Prop} : (∀ᶠ x in pure a, p x) ↔ p a :=
   Iff.rfl
 
+@[simp]
+theorem frequently_pure {a : α} {p : α → Prop} : (∃ᶠ x in pure a, p x) ↔ p a := by
+  simp [Filter.Frequently]
+
 @[simp]
 theorem principal_singleton (a : α) : 𝓟 {a} = pure a :=
   Filter.ext fun s => by simp only [mem_pure, mem_principal, singleton_subset_iff]

Mathlib/Order/Filter/Pointwise.lean

@@ -129,6 +129,10 @@ protected theorem NeBot.le_one_iff (h : f.NeBot) : f ≤ 1 ↔ f = 1 :=
 theorem eventually_one {p : α → Prop} : (∀ᶠ x in 1, p x) ↔ p 1 :=
   eventually_pure
 
+@[to_additive (attr := simp)]
+theorem frequently_one {p : α → Prop} : (∃ᶠ x in 1, p x) ↔ p 1 :=
+  frequently_pure
+
 @[to_additive (attr := simp)]
 theorem tendsto_one {a : Filter β} {f : β → α} : Tendsto f a 1 ↔ ∀ᶠ x in a, f x = 1 :=
   tendsto_pure
@@ -205,6 +209,14 @@ lemma inv.instNeBot [NeBot f] : NeBot f⁻¹ := .inv ‹_›
 
 scoped[Pointwise] attribute [instance] inv.instNeBot neg.instNeBot
 
+@[to_additive (attr := simp)]
+lemma eventually_inv {p : α → Prop} : (∀ᶠ x in f⁻¹, p x) ↔ (∀ᶠ x in f, p x⁻¹) :=
+  eventually_map
+
+@[to_additive (attr := simp)]
+lemma frequently_inv {p : α → Prop} : (∃ᶠ x in f⁻¹, p x) ↔ (∃ᶠ x in f, p x⁻¹) :=
+  frequently_map
+
 end Inv
 
 section InvolutiveInv
@@ -1009,6 +1021,14 @@ lemma smul_filter.instNeBot [NeBot f] : NeBot (a • f) := .smul_filter ‹_›
 
 scoped[Pointwise] attribute [instance] smul_filter.instNeBot vadd_filter.instNeBot
 
+@[to_additive (attr := simp)]
+lemma eventually_smul_filter {p : β → Prop} : (∀ᶠ y in a • f, p y) ↔ (∀ᶠ x in f, p (a • x)) :=
+  eventually_map
+
+@[to_additive (attr := simp)]
+lemma frequently_inv_filter {p : β → Prop} : (∃ᶠ y in a • f, p y) ↔ (∃ᶠ x in f, p (a • x)) :=
+  frequently_map
+
 @[to_additive (attr := gcongr)]
 theorem smul_filter_le_smul_filter (hf : f₁ ≤ f₂) : a • f₁ ≤ a • f₂ :=
   map_mono hf