From 76bb42575dd58c258aea47f9ecc287afca5325e2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 27 Jun 2024 21:04:12 +0000
Subject: [PATCH] chore(Order/Filter/Basic): assert_not_exists OrderedSemiring
 (#14179)

---
 Mathlib.lean                                  |  1 +
 .../Function/AEEqOfIntegral.lean              |  1 +
 Mathlib/Order/Filter/Basic.lean               | 26 +------
 Mathlib/Order/Filter/Extr.lean                |  1 +
 Mathlib/Order/Filter/FilterProduct.lean       |  2 +-
 Mathlib/Order/Filter/Germ.lean                | 29 +------
 Mathlib/Order/Filter/Ring.lean                | 77 +++++++++++++++++++
 7 files changed, 84 insertions(+), 53 deletions(-)
 create mode 100644 Mathlib/Order/Filter/Ring.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index d41fc4deb9895..6f587e48079e2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3349,6 +3349,7 @@ import Mathlib.Order.Filter.Partial
 import Mathlib.Order.Filter.Pi
 import Mathlib.Order.Filter.Pointwise
 import Mathlib.Order.Filter.Prod
+import Mathlib.Order.Filter.Ring
 import Mathlib.Order.Filter.SmallSets
 import Mathlib.Order.Filter.Subsingleton
 import Mathlib.Order.Filter.Ultrafilter
diff --git a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
index 56e3216b932a3..a25897327e3c7 100644
--- a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
+++ b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
@@ -7,6 +7,7 @@ import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.NormedSpace.Dual
 import Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
 import Mathlib.MeasureTheory.Integral.SetIntegral
+import Mathlib.Order.Filter.Ring
 
 #align_import measure_theory.function.ae_eq_of_integral from "leanprover-community/mathlib"@"915591b2bb3ea303648db07284a161a7f2a9e3d4"
 
diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean
index f37f06e139ab5..4ab9c7ecc8cb7 100644
--- a/Mathlib/Order/Filter/Basic.lean
+++ b/Mathlib/Order/Filter/Basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jeremy Avigad
 -/
-import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Data.Set.Finite
 
 #align_import order.filter.basic from "leanprover-community/mathlib"@"d4f691b9e5f94cfc64639973f3544c95f8d5d494"
@@ -78,6 +77,8 @@ we do *not* require. This gives `Filter X` better formal properties, in particul
 `[NeBot f]` in a number of lemmas and definitions.
 -/
 
+assert_not_exists OrderedSemiring
+
 set_option autoImplicit true
 
 
@@ -1871,29 +1872,6 @@ theorem set_eventuallyEq_iff_inf_principal {s t : Set α} {l : Filter α} :
   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
-  filter_upwards [hf, hg, hg₀, hf₀] with x using _root_.mul_le_mul
-#align filter.eventually_le.mul_le_mul Filter.EventuallyLE.mul_le_mul
-
-@[to_additive EventuallyLE.add_le_add]
-theorem EventuallyLE.mul_le_mul' [Mul β] [Preorder β] [CovariantClass β β (· * ·) (· ≤ ·)]
-    [CovariantClass β β (swap (· * ·)) (· ≤ ·)] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β}
-    (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂ := by
-  filter_upwards [hf, hg] with x hfx hgx using _root_.mul_le_mul' hfx hgx
-#align filter.eventually_le.mul_le_mul' Filter.EventuallyLE.mul_le_mul'
-#align filter.eventually_le.add_le_add Filter.EventuallyLE.add_le_add
-
-theorem EventuallyLE.mul_nonneg [OrderedSemiring β] {l : Filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f)
-    (hg : 0 ≤ᶠ[l] g) : 0 ≤ᶠ[l] f * g := by filter_upwards [hf, hg] with x using _root_.mul_nonneg
-#align filter.eventually_le.mul_nonneg Filter.EventuallyLE.mul_nonneg
-
-theorem eventually_sub_nonneg [OrderedRing β] {l : Filter α} {f g : α → β} :
-    0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g :=
-  eventually_congr <| eventually_of_forall fun _ => sub_nonneg
-#align filter.eventually_sub_nonneg Filter.eventually_sub_nonneg
-
 theorem EventuallyLE.sup [SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂)
     (hg : g₁ ≤ᶠ[l] g₂) : f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂ := by
   filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx
diff --git a/Mathlib/Order/Filter/Extr.lean b/Mathlib/Order/Filter/Extr.lean
index 94f8fa5cee4b1..a2b5edbc49d86 100644
--- a/Mathlib/Order/Filter/Extr.lean
+++ b/Mathlib/Order/Filter/Extr.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Order.Filter.Basic
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Algebra.Order.Group.Defs
 
 #align_import order.filter.extr from "leanprover-community/mathlib"@"1f0096e6caa61e9c849ec2adbd227e960e9dff58"
 
diff --git a/Mathlib/Order/Filter/FilterProduct.lean b/Mathlib/Order/Filter/FilterProduct.lean
index 1461bf45a8367..478a237ecd502 100644
--- a/Mathlib/Order/Filter/FilterProduct.lean
+++ b/Mathlib/Order/Filter/FilterProduct.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abhimanyu Pallavi Sudhir, Yury Kudryashov
 -/
 import Mathlib.Order.Filter.Ultrafilter
-import Mathlib.Order.Filter.Germ
+import Mathlib.Order.Filter.Ring
 
 #align_import order.filter.filter_product from "leanprover-community/mathlib"@"2738d2ca56cbc63be80c3bd48e9ed90ad94e947d"
 
diff --git a/Mathlib/Order/Filter/Germ.lean b/Mathlib/Order/Filter/Germ.lean
index e30f771342efa..d4de70af92b6d 100644
--- a/Mathlib/Order/Filter/Germ.lean
+++ b/Mathlib/Order/Filter/Germ.lean
@@ -51,6 +51,7 @@ For each of the following structures we prove that if `β` has this structure, t
 filter, germ
 -/
 
+assert_not_exists OrderedSemiring
 
 namespace Filter
 
@@ -842,11 +843,6 @@ instance instOrderedCancelCommMonoid [OrderedCancelCommMonoid β] :
   le_of_mul_le_mul_left f g h := inductionOn₃ f g h fun _f _g _h H ↦ H.mono
     fun _x ↦ le_of_mul_le_mul_left'
 
-@[to_additive]
-instance instOrderedCommGroup [OrderedCommGroup β] : OrderedCommGroup (Germ l β) where
-  __ := instOrderedCancelCommMonoid
-  __ := instCommGroup
-
 @[to_additive]
 instance instExistsMulOfLE [Mul β] [LE β] [ExistsMulOfLE β] : ExistsMulOfLE (Germ l β) where
   exists_mul_of_le {x y} := inductionOn₂ x y fun f g (h : f ≤ᶠ[l] g) ↦ by
@@ -862,29 +858,6 @@ instance instCanonicallyOrderedCommMonoid [CanonicallyOrderedCommMonoid β] :
   __ := instExistsMulOfLE
   le_self_mul x y := inductionOn₂ x y fun _ _ ↦ eventually_of_forall fun _ ↦ le_self_mul
 
-instance instOrderedSemiring [OrderedSemiring β] : OrderedSemiring (Germ l β) where
-  __ := instSemiring
-  __ := instOrderedAddCommMonoid
-  zero_le_one := const_le zero_le_one
-  mul_le_mul_of_nonneg_left x y z := inductionOn₃ x y z fun _f _g _h hfg hh ↦ hh.mp <| hfg.mono
-    fun _a ↦ mul_le_mul_of_nonneg_left
-  mul_le_mul_of_nonneg_right x y z := inductionOn₃ x y z fun _f _g _h hfg hh ↦ hh.mp <| hfg.mono
-    fun _a ↦ mul_le_mul_of_nonneg_right
-
-instance instOrderedCommSemiring [OrderedCommSemiring β] : OrderedCommSemiring (Germ l β) where
-  __ := instOrderedSemiring
-  __ := instCommSemiring
-
-instance instOrderedRing [OrderedRing β] : OrderedRing (Germ l β) where
-  __ := instRing
-  __ := instOrderedAddCommGroup
-  __ := instOrderedSemiring
-  mul_nonneg x y := inductionOn₂ x y fun _f _g hf hg ↦ hg.mp <| hf.mono fun _a ↦ mul_nonneg
-
-instance instOrderedCommRing [OrderedCommRing β] : OrderedCommRing (Germ l β) where
-  __ := instOrderedRing
-  __ := instOrderedCommSemiring
-
 end Germ
 
 end Filter
diff --git a/Mathlib/Order/Filter/Ring.lean b/Mathlib/Order/Filter/Ring.lean
new file mode 100644
index 0000000000000..e29734064286b
--- /dev/null
+++ b/Mathlib/Order/Filter/Ring.lean
@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Jeremy Avigad
+-/
+import Mathlib.Order.Filter.Germ
+import Mathlib.Algebra.Order.Ring.Defs
+
+/-!
+# Lemmas about filters and ordered rings.
+-/
+namespace Filter
+
+open Function Filter
+
+universe u v
+
+variable {α : Type u} {β : Type v}
+
+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
+  filter_upwards [hf, hg, hg₀, hf₀] with x using _root_.mul_le_mul
+#align filter.eventually_le.mul_le_mul Filter.EventuallyLE.mul_le_mul
+
+@[to_additive EventuallyLE.add_le_add]
+theorem EventuallyLE.mul_le_mul' [Mul β] [Preorder β] [CovariantClass β β (· * ·) (· ≤ ·)]
+    [CovariantClass β β (swap (· * ·)) (· ≤ ·)] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β}
+    (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂ := by
+  filter_upwards [hf, hg] with x hfx hgx using _root_.mul_le_mul' hfx hgx
+#align filter.eventually_le.mul_le_mul' Filter.EventuallyLE.mul_le_mul'
+#align filter.eventually_le.add_le_add Filter.EventuallyLE.add_le_add
+
+theorem EventuallyLE.mul_nonneg [OrderedSemiring β] {l : Filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f)
+    (hg : 0 ≤ᶠ[l] g) : 0 ≤ᶠ[l] f * g := by filter_upwards [hf, hg] with x using _root_.mul_nonneg
+#align filter.eventually_le.mul_nonneg Filter.EventuallyLE.mul_nonneg
+
+theorem eventually_sub_nonneg [OrderedRing β] {l : Filter α} {f g : α → β} :
+    0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g :=
+  eventually_congr <| eventually_of_forall fun _ => sub_nonneg
+#align filter.eventually_sub_nonneg Filter.eventually_sub_nonneg
+
+namespace Germ
+
+variable {l : Filter α}
+
+@[to_additive]
+instance instOrderedCommGroup [OrderedCommGroup β] : OrderedCommGroup (Germ l β) where
+  __ := instOrderedCancelCommMonoid
+  __ := instCommGroup
+
+instance instOrderedSemiring [OrderedSemiring β] : OrderedSemiring (Germ l β) where
+  __ := instSemiring
+  __ := instOrderedAddCommMonoid
+  zero_le_one := const_le zero_le_one
+  mul_le_mul_of_nonneg_left x y z := inductionOn₃ x y z fun _f _g _h hfg hh ↦ hh.mp <| hfg.mono
+    fun _a ↦ mul_le_mul_of_nonneg_left
+  mul_le_mul_of_nonneg_right x y z := inductionOn₃ x y z fun _f _g _h hfg hh ↦ hh.mp <| hfg.mono
+    fun _a ↦ mul_le_mul_of_nonneg_right
+
+instance instOrderedCommSemiring [OrderedCommSemiring β] : OrderedCommSemiring (Germ l β) where
+  __ := instOrderedSemiring
+  __ := instCommSemiring
+
+instance instOrderedRing [OrderedRing β] : OrderedRing (Germ l β) where
+  __ := instRing
+  __ := instOrderedAddCommGroup
+  __ := instOrderedSemiring
+  mul_nonneg x y := inductionOn₂ x y fun _f _g hf hg ↦ hg.mp <| hf.mono fun _a ↦ mul_nonneg
+
+instance instOrderedCommRing [OrderedCommRing β] : OrderedCommRing (Germ l β) where
+  __ := instOrderedRing
+  __ := instOrderedCommSemiring
+
+end Germ
+
+end Filter