Move 3 lemmas back to fix compile

urkud · urkud · commit 7592d0f53e73 · 2024-11-29T12:57:23.000-06:00
diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean
@@ -646,6 +646,10 @@ theorem eventually_or_distrib_right {f : Filter α} {p : α → Prop} {q : Prop}
     (∀ᶠ x in f, p x ∨ q) ↔ (∀ᶠ x in f, p x) ∨ q := by
   simp only [@or_comm _ q, eventually_or_distrib_left]
 
+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]
+
 @[simp]
 theorem eventually_bot {p : α → Prop} : ∀ᶠ x in ⊥, p x :=
   ⟨⟩
@@ -798,6 +802,16 @@ theorem eventually_imp_distrib_right {f : Filter α} {p : α → Prop} {q : Prop
     (∀ᶠ x in f, p x → q) ↔ (∃ᶠ x in f, p x) → q := by
   simp only [imp_iff_not_or, eventually_or_distrib_right, not_frequently]
 
+@[simp]
+theorem frequently_and_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
+    (∃ᶠ x in f, p ∧ q x) ↔ p ∧ ∃ᶠ x in f, q x := by
+  simp only [Filter.Frequently, not_and, eventually_imp_distrib_left, Classical.not_imp]
+
+@[simp]
+theorem frequently_and_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
+    (∃ᶠ x in f, p x ∧ q) ↔ (∃ᶠ x in f, p x) ∧ q := by
+  simp only [@and_comm _ q, frequently_and_distrib_left]
+
 @[simp]
 theorem frequently_bot {p : α → Prop} : ¬∃ᶠ x in ⊥, p x := by simp
 
diff --git a/Mathlib/Order/Filter/Finite.lean b/Mathlib/Order/Filter/Finite.lean
@@ -263,23 +263,6 @@ alias _root_.Finset.eventually_all := eventually_all_finset
 
 -- attribute [protected] Finset.eventually_all
 
-theorem eventually_imp_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
-    (∀ᶠ x in f, p → q x) ↔ p → ∀ᶠ x in f, q x :=
-  eventually_all
-
-
-/-! ### Frequently -/
-
-@[simp]
-theorem frequently_and_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
-    (∃ᶠ x in f, p ∧ q x) ↔ p ∧ ∃ᶠ x in f, q x := by
-  simp only [Filter.Frequently, not_and, eventually_imp_distrib_left, Classical.not_imp]
-
-@[simp]
-theorem frequently_and_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
-    (∃ᶠ x in f, p x ∧ q) ↔ (∃ᶠ x in f, p x) ∧ q := by
-  simp only [@and_comm _ q, frequently_and_distrib_left]
-
 /-!
 ### Relation “eventually equal”
 -/
