chore(Algebra/Order/Module/Defs): don't import fields (#25584)

Instead move the few `Field` lemmas to a new file `Algebra.Order.Module.Field` (leanprover-community/mathlib3#9077 for the copyright) and the `positivity` extension to `Tactic.Positivity.Basic`.

Author: YaelDillies

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -6,6 +6,7 @@ Authors: Jalex Stark, Yury Kudryashov
 import Mathlib.Algebra.BigOperators.Group.Finset.Powerset
 import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Positivity.Basic
 import Mathlib.Tactic.Ring
 
 /-!

Mathlib.lean

@@ -852,6 +852,7 @@ import Mathlib.Algebra.Order.Invertible
 import Mathlib.Algebra.Order.Kleene
 import Mathlib.Algebra.Order.Module.Algebra
 import Mathlib.Algebra.Order.Module.Defs
+import Mathlib.Algebra.Order.Module.Field
 import Mathlib.Algebra.Order.Module.OrderedSMul
 import Mathlib.Algebra.Order.Module.Pointwise
 import Mathlib.Algebra.Order.Module.PositiveLinearMap

Mathlib/Algebra/GeomSum.lean

@@ -5,11 +5,13 @@ Authors: Neil Strickland
 -/
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Group.NatPowAssoc
-import Mathlib.Algebra.Order.BigOperators.Ring.Finset
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Algebra.Ring.Opposite
-import Mathlib.Tactic.Abel
 import Mathlib.Algebra.Ring.Regular
+import Mathlib.Tactic.Abel
+import Mathlib.Tactic.Positivity.Basic
 
 /-!
 # Partial sums of geometric series
@@ -427,7 +429,7 @@ theorem Nat.pred_mul_geom_sum_le (a b n : ℕ) :
   calc
     ((b - 1) * ∑ i ∈ range n.succ, a / b ^ i) =
     (∑ i ∈ range n, a / b ^ (i + 1) * b) + a * b - ((∑ i ∈ range n, a / b ^ i) + a / b ^ n) := by
-      rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
+      rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
         Nat.div_one]
     _ ≤ (∑ i ∈ range n, a / b ^ i) + a * b - ((∑ i ∈ range n, a / b ^ i) + a / b ^ n) := by
       gcongr with i hi

Mathlib/Algebra/MvPolynomial/Degrees.lean

@@ -475,8 +475,8 @@ lemma totalDegree_finsetSum_le {ι : Type*} {s : Finset ι} {f : ι → MvPolyno
   (totalDegree_finset_sum ..).trans <| Finset.sup_le hf
 
 lemma degreeOf_le_totalDegree (f : MvPolynomial σ R) (i : σ) : f.degreeOf i ≤ f.totalDegree :=
-  degreeOf_le_iff.mpr fun d hd ↦ (eq_or_ne (d i) 0).elim (·.trans_le zero_le') fun h ↦
-    (Finset.single_le_sum (fun _ _ ↦ zero_le') <| Finsupp.mem_support_iff.mpr h).trans
+  degreeOf_le_iff.mpr fun d hd ↦ (eq_or_ne (d i) 0).elim (by omega) fun h ↦
+    (Finset.single_le_sum (by omega) <| Finsupp.mem_support_iff.mpr h).trans
     (le_totalDegree hd)
 
 theorem exists_degree_lt [Fintype σ] (f : MvPolynomial σ R) (n : ℕ)

Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean

@@ -6,12 +6,12 @@ Authors: Bolton Bailey, Yaël Dillies, Andrew Yang
 import Mathlib.Algebra.BigOperators.Field
 import Mathlib.Algebra.MvPolynomial.Equiv
 import Mathlib.Algebra.MvPolynomial.Variables
-import Mathlib.Algebra.Order.Group.Finset
 import Mathlib.Algebra.Order.GroupWithZero.Finset
 import Mathlib.Algebra.Order.Ring.Finset
 import Mathlib.Algebra.Polynomial.Roots
 import Mathlib.Data.Fin.Tuple.Finset
 import Mathlib.Tactic.Positivity.Finset
+import Mathlib.Tactic.GCongr
 
 /-!
 # The Schwartz-Zippel lemma

Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Algebra.Order.Hom.Basic
 import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Algebra.Regular.Basic
-import Mathlib.Tactic.Bound.Attribute
+import Mathlib.Tactic.Positivity.Core
 
 /-!
 # Absolute values

Mathlib/Algebra/Order/BigOperators/Expect.lean

@@ -6,7 +6,9 @@ Authors: Yaël Dillies
 import Mathlib.Algebra.BigOperators.Expect
 import Mathlib.Algebra.Module.Rat
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
+import Mathlib.Algebra.Order.Module.Field
 import Mathlib.Algebra.Order.Module.Rat
+import Mathlib.Tactic.GCongr
 
 /-!
 # Order properties of the average over a finset

Mathlib/Algebra/Order/CauSeq/Basic.lean

@@ -31,7 +31,7 @@ This is a concrete implementation that is useful for simplicity and computabilit
 sequence, cauchy, abs val, absolute value
 -/
 
-assert_not_exists Finset Module Submonoid FloorRing Module
+assert_not_exists Finset Module Submonoid FloorRing
 
 variable {α β : Type*}
 
@@ -76,6 +76,7 @@ theorem rat_inv_continuous_lemma {β : Type*} [DivisionRing β] (abv : β → α
   rw [mul_assoc, inv_mul_cancel_right₀ b0.ne', ← mul_assoc, mul_inv_cancel₀ a0.ne', one_mul]
   refine h.trans_le ?_
   gcongr
+  exact mul_nonneg a0.le ε0.le
 
 end
 

Mathlib/Algebra/Order/CauSeq/BigOperators.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes, Yaël Dillies
 -/
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.Order.Archimedean.Basic
+import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.CauSeq.Basic
 
 /-!

Mathlib/Algebra/Order/Floor/Div.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.GroupWithZero.Action.Pi
-import Mathlib.Algebra.Order.Module.Defs
-import Mathlib.Algebra.Order.Pi
 import Mathlib.Data.Finsupp.Order
 
 /-!