feat: forward-port PR 19070 (#4327)

Forward-port leanprover-community/mathlib#19070:

- add `Filter.set_eventuallyLE_iff_mem_inf_principal`,
`Filter.set_eventuallyLE_iff_inf_principal_le`, and
`Filter.set_eventuallyEq_iff_inf_principal`;
- golf `nhdsWithin_eq_iff_eventuallyEq` and `nhdsWithin_le_iff`.

The original PR golfs one more lemma which was already golfed to 1
line in Mathlib 4.

Mathlib/Order/Filter/Basic.lean

@@ -1732,6 +1732,22 @@ theorem EventuallyLE.diff {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l]
   h.inter h'.compl
 #align filter.eventually_le.diff Filter.EventuallyLE.diff
 
+theorem set_eventuallyLE_iff_mem_inf_principal {s t : Set α} {l : Filter α} :
+    s ≤ᶠ[l] t ↔ t ∈ l ⊓ 𝓟 s :=
+  eventually_inf_principal.symm
+#align filter.set_eventually_le_iff_mem_inf_principal Filter.set_eventuallyLE_iff_mem_inf_principal
+
+theorem set_eventuallyLE_iff_inf_principal_le {s t : Set α} {l : Filter α} :
+    s ≤ᶠ[l] t ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t :=
+  set_eventuallyLE_iff_mem_inf_principal.trans <| by
+    simp only [le_inf_iff, inf_le_left, true_and_iff, le_principal_iff]
+#align filter.set_eventually_le_iff_inf_principal_le Filter.set_eventuallyLE_iff_inf_principal_le
+
+theorem set_eventuallyEq_iff_inf_principal {s t : Set α} {l : Filter α} :
+    s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t := by
+  simp only [eventuallyLE_antisymm_iff, le_antisymm_iff, set_eventuallyLE_iff_inf_principal_le]
+#align filter.set_eventually_eq_iff_inf_principal Filter.set_eventuallyEq_iff_inf_principal
+
 theorem EventuallyLE.mul_le_mul [MulZeroClass β] [PartialOrder β] [PosMulMono β] [MulPosMono β]
     {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁)
     (hf₀ : 0 ≤ᶠ[l] f₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂ := by

Mathlib/Topology/ContinuousOn.lean

@@ -128,22 +128,12 @@ theorem mem_nhdsWithin_iff_eventuallyEq {s t : Set α} {x : α} :
   simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]
 #align mem_nhds_within_iff_eventually_eq mem_nhdsWithin_iff_eventuallyEq
 
-theorem nhdsWithin_eq_iff_eventuallyEq {s t : Set α} {x : α} : 𝓝[s] x = 𝓝[t] x ↔ s =ᶠ[𝓝 x] t := by
-  simp_rw [Filter.ext_iff, mem_nhdsWithin_iff_eventually, eventuallyEq_set]
-  constructor
-  · intro h
-    filter_upwards [(h t).mpr (eventually_of_forall fun x => id),
-      (h s).mp (eventually_of_forall fun x => id)]
-    exact fun x => Iff.intro
-  · refine' fun h u => eventually_congr (h.mono fun x h => _)
-    rw [h]
+theorem nhdsWithin_eq_iff_eventuallyEq {s t : Set α} {x : α} : 𝓝[s] x = 𝓝[t] x ↔ s =ᶠ[𝓝 x] t :=
+  set_eventuallyEq_iff_inf_principal.symm
 #align nhds_within_eq_iff_eventually_eq nhdsWithin_eq_iff_eventuallyEq
 
-theorem nhdsWithin_le_iff {s t : Set α} {x : α} : 𝓝[s] x ≤ 𝓝[t] x ↔ t ∈ 𝓝[s] x := by
-  simp_rw [Filter.le_def, mem_nhdsWithin_iff_eventually]
-  constructor
-  · exact fun h => (h t <| eventually_of_forall fun x => id).mono fun x => id
-  · exact fun h u hu => (h.and hu).mono fun x hx h => hx.2 <| hx.1 h
+theorem nhdsWithin_le_iff {s t : Set α} {x : α} : 𝓝[s] x ≤ 𝓝[t] x ↔ t ∈ 𝓝[s] x :=
+  set_eventuallyLE_iff_inf_principal_le.symm.trans set_eventuallyLE_iff_mem_inf_principal
 #align nhds_within_le_iff nhdsWithin_le_iff
 
 -- porting note: golfed, droped an unneeded assumption