refactor(real-roots-mathlib): use Mathlib list sign variations

HexIntervalMathlib/Experiment/PntBKLNWExp.lean

@@ -192,7 +192,6 @@ theorem expSumWithTail {b N : Nat} (atLeast : 64 ≤ N) :
       _ = ((N - 63 : Nat) : ℝ) * upperBaseValue 64 ^ b := by
         congr 2
         norm_num [Nat.card_Icc]
-        omega
   constructor
   · calc
       1 + lowerBand b 63 ≤

HexIntervalMathlib/Experiment/PntBKLNWPow.lean

@@ -110,7 +110,6 @@ theorem powSumUpper {M a b : Nat} (hM : 5 ≤ M)
     _ = ((M - 4 : Nat) : ℝ) / (2 : ℝ) ^ b := by
       congr 2
       norm_num [Nat.card_Icc]
-      omega
 
 private theorem alphaRatio :
     (1 + 193571378 / (10 : ℝ) ^ 16) =
@@ -317,7 +316,6 @@ theorem finePowSumUpper {M : Nat} (hM : 21 ≤ M) :
       _ = ((M - 20 : Nat) : ℝ) * baseValue 21 ^ M := by
         congr 2
         norm_num [Nat.card_Icc]
-        omega
 
 private theorem exactBaseRatio (M : Nat) :
     exactBaseSum M =

HexIntervalMathlib/Experiment/PntTable10A2.lean

@@ -210,7 +210,6 @@ private theorem expSumUpper (value : Certificate) (valid : Valid value) :
           PntBKLNWExp.upperBaseValue 13 ^ value.argument := by
         congr 2
         norm_num [Nat.card_Icc, tailCardinality]
-        omega
   linarith
 
 private theorem sourceExpLeSucc (value : Certificate) (valid : Valid value) :

HexMatrixMathlib/Hadamard.lean

@@ -96,7 +96,7 @@ theorem norm_det_le_prod_norm_column (A : Matrix n n 𝕜) :
   -- Cauchy-Schwarz on each diagonal factor.
   have hbound : ‖e.toBasis.det f‖ ≤ ∏ j, ‖f j‖ := by
     rw [hdet, norm_prod]
-    refine Finset.prod_le_prod (fun i _ => norm_nonneg _) (fun i _ => ?_)
+    refine Finset.prod_le_prod₀ (fun i _ => norm_nonneg _) (fun i _ => ?_)
     calc ‖inner 𝕜 (e i) (f i)‖ ≤ ‖e i‖ * ‖f i‖ := norm_inner_le_norm _ _
       _ = ‖f i‖ := by rw [e.orthonormal.norm_eq_one, one_mul]
   calc ‖A.det‖ = ‖e.toBasis.det f‖ := hchange.symm

HexMatrixMathlib/Literal.lean

@@ -281,7 +281,7 @@ def evalEntry (e : Expr) : MetaM Rat := do
   catch _ =>
     let ctx ← Simp.mkContext (config := { decide := true })
       (simpTheorems := #[← getSimpTheorems]) (congrTheorems := ← getSimpCongrTheorems)
-    let r ← Mathlib.Meta.NormNum.deriveSimp ctx true e
+    let r ← Mathlib.Meta.NormNum.deriveSimp ctx #[] true e
     Mathlib.Tactic.Echelon.evalRatEntry true r.expr
 
 /-- Evaluate every entry to a rational. -/

HexModularMatrixMathlib/Bound.lean

@@ -50,7 +50,7 @@ private theorem column_bound (A : Hex.Matrix Int n n) :
     exact_mod_cast HexArith.Nat.le_ceilSqrt_sq
       (Hex.Matrix.DetBound.sum (fun i : Fin n => A[(i, j)].natAbs ^ 2))
   have h := (Matrix.norm_det_le_prod_norm_column B).trans
-    (Finset.prod_le_prod (fun _ _ => Real.sqrt_nonneg _) (fun j _ => hc j))
+    (Finset.prod_le_prod₀ (fun _ _ => Real.sqrt_nonneg _) (fun j _ => hc j))
   rw [hd] at h
   rw [prod_eq]
   exact_mod_cast (by simpa only [Nat.cast_natAbs, Int.cast_abs, Real.norm_eq_abs, Nat.cast_prod] using h :

HexMvPolyMathlib/Equiv.lean

@@ -152,7 +152,7 @@ theorem toMvPolynomial_eq_sum [CommSemiring R] [DecidableEq R]
 /-- Forward conversion preserves every coefficient. -/
 @[simp] theorem coeff_toMvPolynomial [CommSemiring R] [DecidableEq R]
     (m : Mono n) (p : MvPoly n R cmp) :
-    MvPolynomial.coeff (monoEquiv m) (toMvPolynomial p) = coeff m p := by
+    (toMvPolynomial p).coeff (monoEquiv m) = coeff m p := by
   rw [toMvPolynomial, MvPolynomial.coeff_sum]
   simp [MvPolynomial.coeff_monomial, monoEquiv.injective.eq_iff,
     mem_monomials_iff, eq_comm]
@@ -243,13 +243,13 @@ polynomial's finite support. -/
 def ofMvPolynomial [CommSemiring R] [DecidableEq R]
     (p : MvPolynomial (Fin n) R) : MvPoly n R cmp :=
   ofTerms <| p.support.toList.map fun d =>
-    (monoEquiv.symm d, MvPolynomial.coeff d p)
+    (monoEquiv.symm d, p.coeff d)
 
 /-- Backward conversion preserves every coefficient. -/
 @[simp] theorem coeff_ofMvPolynomial [CommSemiring R] [DecidableEq R]
     (m : Mono n) (p : MvPolynomial (Fin n) R) :
     coeff m (ofMvPolynomial (cmp := cmp) p) =
-      MvPolynomial.coeff (monoEquiv m) p := by
+      p.coeff (monoEquiv m) := by
   rw [ofMvPolynomial, coeff_ofTerms]
   rw [List.foldl_filter, List.foldl_map]
   simp only [Equiv.symm_apply_eq]
@@ -276,9 +276,9 @@ def ofMvPolynomial [CommSemiring R] [DecidableEq R]
         · have hqd : q ≠ d := Ne.symm hdq
           rw [ite_eq_right (by simp [hdq]), ih hds]
           simp [hqd]
-  rw [fold_pick (monoEquiv m) (fun d => MvPolynomial.coeff d p)
+  rw [fold_pick (monoEquiv m) (fun d => p.coeff d)
     p.support.toList p.support.nodup_toList]
-  by_cases hcoeff : MvPolynomial.coeff (monoEquiv m) p = 0
+  by_cases hcoeff : p.coeff (monoEquiv m) = 0
   · simp [hcoeff]
   · simp [hcoeff]
 

HexMvPolyMathlib/Recursive.lean

@@ -85,7 +85,7 @@ theorem recursiveMap_injective [CommSemiring R] [DecidableEq R] :
   intro m
   have hc := congrArg
     (fun f =>
-      MvPolynomial.coeff (monoEquiv m) (Polynomial.coeff f e)) h
+      (Polynomial.coeff f e).coeff (monoEquiv m)) h
   simpa [recursiveMap] using hc
 
 /-- The comparison map preserves zero. -/

HexNumberFieldMathlib/Interval.lean

@@ -14,10 +14,10 @@ open HexRootsMathlib
 
 /-- Both coordinate projections lie in the dyadic radius bounds. -/
 theorem bounds {p : ZPoly} (a : RefinedIsolation p) :
-    (Dyadic.toReal (a.1.square.re - a.1.square.radiusHi) ≤ a.root.re ∧
-      a.root.re ≤ Dyadic.toReal (a.1.square.re + a.1.square.radiusHi)) ∧
-    (Dyadic.toReal (a.1.square.im - a.1.square.radiusHi) ≤ a.root.im ∧
-      a.root.im ≤ Dyadic.toReal (a.1.square.im + a.1.square.radiusHi)) := by
+    (HexRootsMathlib.Dyadic.toReal (a.1.square.re - a.1.square.radiusHi) ≤ a.root.re ∧
+      a.root.re ≤ HexRootsMathlib.Dyadic.toReal (a.1.square.re + a.1.square.radiusHi)) ∧
+    (HexRootsMathlib.Dyadic.toReal (a.1.square.im - a.1.square.radiusHi) ≤ a.root.im ∧
+      a.root.im ≤ HexRootsMathlib.Dyadic.toReal (a.1.square.im + a.1.square.radiusHi)) := by
   have hd := RefinedIsolation.root_mem_closedDisc a
   change dist a.root (HexRootsMathlib.DyadicSquare.center a.1.square) ≤ HexRootsMathlib.DyadicSquare.radius a.1.square at hd
   rw [dist_eq_norm] at hd
@@ -27,7 +27,7 @@ theorem bounds {p : ZPoly} (a : RefinedIsolation p) :
     (hd.trans (DyadicSquare.radius_lt_radiusHi _).le)
   simp only [Complex.sub_re, Complex.sub_im, DyadicSquare.center_eq,
     Hex.DyadicSquare.center, GaussDyadic.toComplex] at hre him
-  simp only [Dyadic.toReal_sub, Dyadic.toReal_add]
+  simp only [HexRootsMathlib.Dyadic.toReal_sub, HexRootsMathlib.Dyadic.toReal_add]
   obtain ⟨hrl, hru⟩ := abs_le.mp hre
   obtain ⟨hil, hiu⟩ := abs_le.mp him
   constructor <;> constructor <;> linarith
@@ -42,12 +42,12 @@ theorem realOrder?_sound {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsol
   split at h
   · rename_i hlt
     have : a.root.re < b.root.re := lt_of_le_of_lt ha.1.2
-      ((Dyadic.toReal_lt_toReal_iff.mpr hlt).trans_le hb.1.1)
+      ((HexRootsMathlib.Dyadic.toReal_lt_toReal_iff.mpr hlt).trans_le hb.1.1)
     exact (compare_lt_iff_lt.mpr this).trans (Option.some.inj h)
   · split at h
     · rename_i hgt
       have : b.root.re < a.root.re := lt_of_le_of_lt hb.1.2
-        ((Dyadic.toReal_lt_toReal_iff.mpr hgt).trans_le ha.1.1)
+        ((HexRootsMathlib.Dyadic.toReal_lt_toReal_iff.mpr hgt).trans_le ha.1.1)
       exact (compare_gt_iff_gt.mpr this).trans (Option.some.inj h)
     · contradiction
 
@@ -58,24 +58,24 @@ theorem imagApart_sound {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsola
   have hb := (bounds b).2
   simp only [imagApart, Bool.or_eq_true, decide_eq_true_eq] at h
   rcases h with h | h
-  · exact ne_of_lt (ha.2.trans_lt ((Dyadic.toReal_lt_toReal_iff.mpr h).trans_le hb.1))
-  · exact ne_of_gt (hb.2.trans_lt ((Dyadic.toReal_lt_toReal_iff.mpr h).trans_le ha.1))
+  · exact ne_of_lt (ha.2.trans_lt ((HexRootsMathlib.Dyadic.toReal_lt_toReal_iff.mpr h).trans_le hb.1))
+  · exact ne_of_gt (hb.2.trans_lt ((HexRootsMathlib.Dyadic.toReal_lt_toReal_iff.mpr h).trans_le ha.1))
 
 /-- A strict-order rejection is sound. -/
 theorem notLt_sound {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q)
     (h : notLt a.1.square b.1.square = true) : ¬ a.root.re < b.root.re := by
   have ha := (bounds a).1
   have hb := (bounds b).1
   simp only [notLt, decide_eq_true_eq] at h
-  exact not_lt_of_ge (hb.2.trans ((Dyadic.toReal_le_toReal_iff.mpr h).trans ha.1))
+  exact not_lt_of_ge (hb.2.trans ((HexRootsMathlib.Dyadic.toReal_le_toReal_iff.mpr h).trans ha.1))
 
 /-- A non-strict-order rejection is sound. -/
 theorem notLe_sound {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q)
     (h : notLe a.1.square b.1.square = true) : ¬ a.root.re ≤ b.root.re := by
   have ha := (bounds a).1
   have hb := (bounds b).1
   simp only [notLe, decide_eq_true_eq] at h
-  exact not_le_of_gt (hb.2.trans_lt ((Dyadic.toReal_lt_toReal_iff.mpr h).trans_le ha.1))
+  exact not_le_of_gt (hb.2.trans_lt ((HexRootsMathlib.Dyadic.toReal_lt_toReal_iff.mpr h).trans_le ha.1))
 
 /-- Threaded refinement preserves any sound coordinate probe. -/
 theorem search_sound {α : Type} (probe : DyadicSquare → DyadicSquare → Option α)

HexNumberFieldMathlib/Nearest.lean

@@ -32,10 +32,10 @@ namespace Hex
 namespace DyadicComplexBall
 
 /-- The centre of a ball, componentwise. -/
-theorem center_re (b : DyadicComplexBall) : b.center.re = Dyadic.toReal b.re :=
+theorem center_re (b : DyadicComplexBall) : b.center.re = HexRootsMathlib.Dyadic.toReal b.re :=
   GaussDyadic.toComplex_re (b.re, b.im)
 
-theorem center_im (b : DyadicComplexBall) : b.center.im = Dyadic.toReal b.im :=
+theorem center_im (b : DyadicComplexBall) : b.center.im = HexRootsMathlib.Dyadic.toReal b.im :=
   GaussDyadic.toComplex_im (b.re, b.im)
 
 /-- A point of a ball is within the radius of the centre. -/
@@ -52,8 +52,8 @@ theorem radius_nonneg_of_mem {b : DyadicComplexBall} {z : ℂ} (h : z ∈ b.set)
 theorem meets_of_mem_set {b₁ b₂ : DyadicComplexBall} {z : ℂ}
     (h₁ : z ∈ b₁.set) (h₂ : z ∈ b₂.set) : b₁.meets b₂ = true := by
   unfold meets
-  rw [decide_eq_true_eq, ← Dyadic.toReal_le_toReal_iff, Dyadic.toReal_mul,
-    Dyadic.toReal_add, DyadicSquare.toReal_distSq]
+  rw [decide_eq_true_eq, ← HexRootsMathlib.Dyadic.toReal_le_toReal_iff, HexRootsMathlib.Dyadic.toReal_mul,
+    HexRootsMathlib.Dyadic.toReal_add, DyadicSquare.toReal_distSq]
   have h₁' := dist_le_of_mem h₁
   have h₂' := dist_le_of_mem h₂
   have htri : dist b₁.center b₂.center ≤ b₁.realRadius + b₂.realRadius := by
@@ -70,8 +70,8 @@ theorem dist_le_of_meets {b₁ b₂ : DyadicComplexBall} {z w : ℂ}
     (h : b₁.meets b₂ = true) (hz : z ∈ b₁.set) (hw : w ∈ b₂.set) :
     dist z w ≤ 2 * (b₁.realRadius + b₂.realRadius) := by
   unfold meets at h
-  rw [decide_eq_true_eq, ← Dyadic.toReal_le_toReal_iff, Dyadic.toReal_mul,
-    Dyadic.toReal_add, DyadicSquare.toReal_distSq] at h
+  rw [decide_eq_true_eq, ← HexRootsMathlib.Dyadic.toReal_le_toReal_iff, HexRootsMathlib.Dyadic.toReal_mul,
+    HexRootsMathlib.Dyadic.toReal_add, DyadicSquare.toReal_distSq] at h
   have hnn : 0 ≤ b₁.realRadius + b₂.realRadius :=
     add_nonneg (radius_nonneg_of_mem hz) (radius_nonneg_of_mem hw)
   have hcenters : dist b₁.center b₂.center ≤ b₁.realRadius + b₂.realRadius := by
@@ -101,7 +101,7 @@ theorem conj_mem_mirrorBall {b : DyadicComplexBall} {z : ℂ} (h : z ∈ b.set)
     apply Complex.ext
     · rw [DyadicComplexBall.center_re, Complex.conj_re, DyadicComplexBall.center_re, hre]
     · rw [DyadicComplexBall.center_im, Complex.conj_im, DyadicComplexBall.center_im, him,
-        Dyadic.toReal_neg]
+        HexRootsMathlib.Dyadic.toReal_neg]
   have hradius : (mirrorBall b).realRadius = b.realRadius := rfl
   rw [DyadicComplexBall.set, Metric.mem_closedBall, hcenter, hradius, Complex.dist_conj_conj]
   exact DyadicComplexBall.dist_le_of_mem h
@@ -183,7 +183,7 @@ theorem mul_p_ne_zero (a b : AlgebraicNumber) : a.p * b.p ≠ 0 := by
 
 /-- The real part of a number is within the ball radius of the centre's. -/
 theorem abs_re_sub_center_le (a : AlgebraicNumber) (prec : Int) :
-    |a.toComplex.re - Dyadic.toReal (a.approx prec).re| ≤ (a.approx prec).realRadius := by
+    |a.toComplex.re - HexRootsMathlib.Dyadic.toReal (a.approx prec).re| ≤ (a.approx prec).realRadius := by
   have h := DyadicComplexBall.dist_le_of_mem (approx_mem a prec)
   rw [dist_eq_norm] at h
   have h' := Complex.abs_re_le_norm (a.toComplex - (a.approx prec).center)
@@ -220,17 +220,17 @@ theorem realCompareExact_eq (a b : AlgebraicNumber) (ha : a.isReal = true)
         then Ordering.lt else Ordering.gt) = _
     split
     · rename_i hlt
-      have hlt' := Dyadic.toReal_lt_toReal_iff.mpr hlt
+      have hlt' := HexRootsMathlib.Dyadic.toReal_lt_toReal_iff.mpr hlt
       symm
       rw [compare_lt_iff_lt]
       by_contra hge
       have hge' := not_lt.mp hge
       rw [abs_of_nonneg (by linarith)] at hsep
       linarith
     · rename_i hnlt
-      have hge' : Dyadic.toReal (b.approx (separationPrec (a.p * b.p))).re ≤
-          Dyadic.toReal (a.approx (separationPrec (a.p * b.p))).re :=
-        not_lt.mp fun h => hnlt (Dyadic.toReal_lt_toReal_iff.mp h)
+      have hge' : HexRootsMathlib.Dyadic.toReal (b.approx (separationPrec (a.p * b.p))).re ≤
+          HexRootsMathlib.Dyadic.toReal (a.approx (separationPrec (a.p * b.p))).re :=
+        not_lt.mp fun h => hnlt (HexRootsMathlib.Dyadic.toReal_lt_toReal_iff.mp h)
       symm
       rw [compare_gt_iff_gt]
       by_contra hle
@@ -303,9 +303,9 @@ theorem square_im_pos_iff {d : AlgebraicNumber}
   have hdist : dist d.toComplex (HexRootsMathlib.DyadicSquare.center s) ≤
       HexRootsMathlib.DyadicSquare.radius s := by
     simpa only [HexRootsMathlib.DyadicSquare.closedDisc, Metric.mem_closedBall] using hmem
-  have hcenter : (HexRootsMathlib.DyadicSquare.center s).im = Dyadic.toReal s.im := by
+  have hcenter : (HexRootsMathlib.DyadicSquare.center s).im = HexRootsMathlib.Dyadic.toReal s.im := by
     simp [HexRootsMathlib.DyadicSquare.center_eq, Hex.DyadicSquare.center]
-  have himDist : |d.toComplex.im - Dyadic.toReal s.im| ≤
+  have himDist : |d.toComplex.im - HexRootsMathlib.Dyadic.toReal s.im| ≤
       HexRootsMathlib.DyadicSquare.radius s := by
     have h := Complex.abs_im_le_norm (d.toComplex - HexRootsMathlib.DyadicSquare.center s)
     rw [Complex.sub_im, hcenter] at h
@@ -326,7 +326,7 @@ theorem square_im_pos_iff {d : AlgebraicNumber}
           mul_lt_mul_of_pos_left hsqrt hpos
       _ ≤ (2 : ℝ) ^ (-(3 : ℤ)) * 2 := by gcongr
       _ = 1 / 4 := by norm_num
-  rw [← Dyadic.toReal_lt_toReal_iff, Dyadic.toReal_zero]
+  rw [← HexRootsMathlib.Dyadic.toReal_lt_toReal_iff, HexRootsMathlib.Dyadic.toReal_zero]
   rw [abs_le] at himDist
   rcases hcases with h | h
   · rw [h] at himDist ⊢
@@ -439,7 +439,7 @@ theorem ballDistSq_cast (b : DyadicComplexBall) (re im : Rat) :
   rw [Complex.sq_norm, Complex.normSq_apply, Complex.sub_re, Complex.sub_im,
     DyadicComplexBall.center_re, DyadicComplexBall.center_im]
   simp only [point, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im,
-    Complex.I_re, Complex.I_im, Dyadic.toReal, Complex.ratCast_re, Complex.ratCast_im]
+    Complex.I_re, Complex.I_im, HexRootsMathlib.Dyadic.toReal, Complex.ratCast_re, Complex.ratCast_im]
   push_cast
   ring
 
@@ -453,7 +453,7 @@ theorem norm_center_sub_le (b : DyadicComplexBall) (re im : Rat) :
   rw [Complex.sub_re, Complex.sub_im, DyadicComplexBall.center_re,
     DyadicComplexBall.center_im] at h
   simp only [point, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im,
-    Complex.I_re, Complex.I_im, Dyadic.toReal, Complex.ratCast_re, Complex.ratCast_im] at h
+    Complex.I_re, Complex.I_im, HexRootsMathlib.Dyadic.toReal, Complex.ratCast_re, Complex.ratCast_im] at h
   push_cast
   simpa using h
 

HexPolyZMathlib/MahlerSeparation.lean

@@ -245,7 +245,7 @@ theorem norm_det_vandermonde_le {N : ℕ} (hN : 2 ≤ N) (c : ℂ) (α : Fin N 
     rw [← Finset.mul_prod_erase univ _ (Finset.mem_univ i₁)]
     refine mul_le_mul hRi1 ?_ (Finset.prod_nonneg (fun j _ => Real.sqrt_nonneg _))
       (mul_nonneg (mul_nonneg (pow_nonneg (hB0 i₁) _) (norm_nonneg _)) (Real.sqrt_nonneg _))
-    exact Finset.prod_le_prod (fun j _ => Real.sqrt_nonneg _)
+    exact Finset.prod_le_prod₀ (fun j _ => Real.sqrt_nonneg _)
       (fun j hj => hRj j (Finset.mem_erase.mp hj).1)
   have hprodrw : ∏ j ∈ univ.erase i₁, (Real.sqrt N * B j ^ (N - 1))
       = Real.sqrt N ^ (N - 1) * (∏ j ∈ univ.erase i₁, B j) ^ (N - 1) := by

HexPolyZMathlib/RobinsonForm.lean

@@ -392,7 +392,7 @@ theorem mahlerMeasure_le_circleAverage_norm (p : ℂ[X]) :
   have : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * Real.pi))) := by
     rw [uIoc_of_le (by positivity)]
     infer_instance
-  have : NeZero (volume (uIoc 0 (2 * Real.pi))) := ⟨by simp⟩
+  have : NeZero (volume (uIoc 0 (2 * Real.pi))) := ⟨by simp [Real.pi_pos]⟩
   by_cases hp : p = 0
   · rw [hp, mahlerMeasure_zero]
     exact Real.circleAverage_nonneg_of_nonneg (fun z _ => norm_nonneg (eval z (0 : ℂ[X])))