feat(Order/Filter): Add lemmas about Filter.curry (#12435)

`Filter.curry` is a useful definition for reasoning about Fubini-type theorems, but there are almost no lemmas about it. This PR adds some in preparation for an upcomming PR on the Kuratowski-Ulam theorem.

Author: Felix-Weilacher

Mathlib/Order/Filter/CountableInter.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
-import Mathlib.Order.Filter.Basic
+import Mathlib.Order.Filter.Curry
 import Mathlib.Data.Set.Countable
 
 #align_import order.filter.countable_Inter from "leanprover-community/mathlib"@"b9e46fe101fc897fb2e7edaf0bf1f09ea49eb81a"
@@ -229,6 +229,13 @@ instance countableInterFilter_sup (l₁ l₂ : Filter α) [CountableInterFilter
   exacts [(hS s hs).1, (hS s hs).2]
 #align countable_Inter_filter_sup countableInterFilter_sup
 
+instance CountableInterFilter.curry {α β : Type*} {l : Filter α} {m : Filter β}
+    [CountableInterFilter l] [CountableInterFilter m] : CountableInterFilter (l.curry m) := ⟨by
+  intro S Sct hS
+  simp_rw [mem_curry_iff, mem_sInter, eventually_countable_ball (p := fun _ _ _ => (_ ,_) ∈ _) Sct,
+    eventually_countable_ball (p := fun _ _ _ => ∀ᶠ (_ : β) in m, _)  Sct, ← mem_curry_iff]
+  exact hS⟩
+
 namespace Filter
 
 variable (g : Set (Set α))

Mathlib/Order/Filter/Curry.lean

@@ -64,6 +64,13 @@ theorem eventually_curry_iff {f : Filter α} {g : Filter β} {p : α × β → P
   Iff.rfl
 #align filter.eventually_curry_iff Filter.eventually_curry_iff
 
+theorem frequently_curry_iff {α β : Type*} {l : Filter α} {m : Filter β}
+    (p : (α × β) → Prop) : (∃ᶠ x in l.curry m, p x) ↔ ∃ᶠ x in l, ∃ᶠ y in m, p (x, y) := by
+  simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]
+
+theorem mem_curry_iff {f : Filter α} {g : Filter β} {s : Set (α × β)} :
+    s ∈ f.curry g ↔ ∀ᶠ x : α in f, ∀ᶠ y : β in g, (x, y) ∈ s := Iff.rfl
+
 theorem curry_le_prod {f : Filter α} {g : Filter β} : f.curry g ≤ f.prod g :=
   fun _ => Eventually.curry
 #align filter.curry_le_prod Filter.curry_le_prod
@@ -73,4 +80,26 @@ theorem Tendsto.curry {f : α → β → γ} {la : Filter α} {lb : Filter β} {
   fun _s hs => h.mono fun _a ha => ha hs
 #align filter.tendsto.curry Filter.Tendsto.curry
 
+theorem frequently_curry_prod_iff {α β : Type*} {l : Filter α} {m : Filter β}
+    (s : Set α) (t : Set β) : (∃ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ sᶜ ∉ l ∧ tᶜ ∉ m := by
+  refine ⟨fun h => ?_, fun ⟨hs, ht⟩ => ?_⟩
+  · exact frequently_prod_and.mp (Frequently.filter_mono h curry_le_prod)
+  rw [frequently_curry_iff]
+  exact Frequently.mono hs $ fun x hx => Frequently.mono ht (by simp[hx])
+
+theorem prod_mem_curry {α β : Type*} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β}
+    (hs : s ∈ l) (ht : t ∈ m) : s ×ˢ t ∈ l.curry m :=
+  curry_le_prod $ prod_mem_prod hs ht
+
+theorem eventually_curry_prod_iff {α β : Type*} {l : Filter α} {m : Filter β}
+    [NeBot l] [NeBot m] (s : Set α) (t : Set β) :
+    (∀ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m := by
+  refine ⟨fun h => ⟨?_, ?_⟩, fun ⟨hs, ht⟩ => prod_mem_curry hs ht⟩ <;>
+    rw [eventually_curry_iff] at h
+  · apply mem_of_superset h
+    simp
+  rcases h.exists with ⟨_, hx⟩
+  apply mem_of_superset hx
+  exact fun _ hy => hy.2
+
 end Filter