fix: correct Lean.Grind.NatModule

src/Init/Grind/Ordered/Int.lean

@@ -24,7 +24,7 @@ instance : Preorder Int where
 instance : IntModule.IsOrdered Int where
   neg_le_iff := by omega
   add_le_left := by omega
-  hmul_pos k a ha := ⟨fun hk => Int.mul_pos hk ha, fun h => Int.pos_of_mul_pos_left h ha⟩
+  hmul_pos_iff k a ha := ⟨fun h => Int.pos_of_mul_pos_left h ha, fun hk => Int.mul_pos hk ha⟩
   hmul_nonneg hk ha := Int.mul_nonneg hk ha
 
 instance : Ring.IsOrdered Int where

src/Init/Grind/Ordered/Linarith.lean

@@ -286,7 +286,7 @@ theorem le_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α]
     : le_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
   simp [-Int.natAbs_pos, -Int.ofNat_pos, le_lt_combine_cert]; intro hp _ h₁ h₂; subst p₃; simp
   replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
-  replace h₂ := hmul_neg (↑p₁.leadCoeff.natAbs) h₂ |>.mp hp
+  replace h₂ := hmul_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp
   exact le_add_lt h₁ h₂
 
 def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
@@ -297,8 +297,8 @@ def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
 theorem lt_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
     : lt_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx < 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
   simp [-Int.natAbs_pos, -Int.ofNat_pos, lt_lt_combine_cert]; intro hp₁ hp₂ _ h₁ h₂; subst p₃; simp
-  replace h₁ := hmul_neg (↑p₂.leadCoeff.natAbs) h₁ |>.mp hp₁
-  replace h₂ := hmul_neg (↑p₁.leadCoeff.natAbs) h₂ |>.mp hp₂
+  replace h₁ := hmul_neg_iff (↑p₂.leadCoeff.natAbs) h₁ |>.mpr hp₁
+  replace h₂ := hmul_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp₂
   exact lt_add_lt h₁ h₂
 
 def diseq_split_cert (p₁ p₂ : Poly) : Bool :=
@@ -483,7 +483,7 @@ theorem le_coeff {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (
   have : ↑k > (0 : Int) := Int.natCast_pos.mpr h
   intro h₁; apply Classical.byContradiction
   intro h₂; replace h₂ := LinearOrder.lt_of_not_le h₂
-  replace h₂ := IsOrdered.hmul_pos (↑k) h₂ |>.mp this
+  replace h₂ := IsOrdered.hmul_pos_iff (↑k) h₂ |>.mpr this
   exact Preorder.lt_irrefl 0 (Preorder.lt_of_lt_of_le h₂ h₁)
 
 theorem lt_coeff {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
@@ -550,7 +550,7 @@ def eq_lt_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
 theorem eq_lt_subst {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
     : eq_lt_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
   simp [eq_lt_subst_cert]; intro h _ h₁ h₂; subst p₃; simp [h₁]
-  exact IsOrdered.hmul_neg (p₁.coeff x) h₂ |>.mp h
+  exact IsOrdered.hmul_neg_iff (p₁.coeff x) h₂ |>.mpr h
 
 def eq_eq_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
   let a := p₁.coeff x

src/Init/Grind/Ordered/Module.lean

@@ -14,13 +14,13 @@ namespace Lean.Grind
 
 class NatModule.IsOrdered (M : Type u) [Preorder M] [NatModule M] where
   add_le_left_iff : ∀ {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c
-  hmul_pos : ∀ (k : Nat) {a : M}, 0 < a → (0 < k ↔ 0 < k * a)
-  hmul_nonneg : ∀ {k : Nat} {a : M}, 0 ≤ a → 0 ≤ k * a
+  hmul_lt_hmul_iff : ∀ (k : Nat) {a b : M}, a < b → (k * a < k * b ↔ 0 < k)
+  hmul_le_hmul : ∀ {k : Nat} {a b : M}, a ≤ b → k * a ≤ k * b
 
 class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
   neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
   add_le_left : ∀ {a b : M}, a ≤ b → (c : M) → a + c ≤ b + c
-  hmul_pos : ∀ (k : Int) {a : M}, 0 < a → (0 < k ↔ 0 < k * a)
+  hmul_pos_iff : ∀ (k : Int) {a : M}, 0 < a → (0 < k * a ↔ 0 < k)
   hmul_nonneg : ∀ {k : Int} {a : M}, 0 ≤ k → 0 ≤ a → 0 ≤ k * a
 
 namespace NatModule.IsOrdered
@@ -28,12 +28,12 @@ namespace NatModule.IsOrdered
 variable {M : Type u} [Preorder M] [NatModule M] [NatModule.IsOrdered M]
 
 theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by
-  rw [add_comm c a, add_comm c b,add_le_left_iff]
+  rw [add_comm c a, add_comm c b, add_le_left_iff]
 
 theorem add_le_left {a b : M} (h : a ≤ b) (c : M) : a + c ≤ b + c :=
   (add_le_left_iff c).mp h
 
-theorem add_le_right {a b : M} (h : a ≤ b) (c : M) : c + a ≤ c + b :=
+theorem add_le_right {a b : M} (c : M) (h : a ≤ b) : c + a ≤ c + b :=
   (add_le_right_iff c).mp h
 
 theorem add_lt_left {a b : M} (h : a < b) (c : M) : a + c < b + c := by
@@ -44,7 +44,7 @@ theorem add_lt_left {a b : M} (h : a < b) (c : M) : a + c < b + c := by
     apply h.2
     exact (add_le_left_iff c).mpr w
 
-theorem add_lt_right {a b : M} (h : a < b) (c : M) : c + a < c + b := by
+theorem add_lt_right {a b : M} (c : M) (h : a < b) : c + a < c + b := by
   rw [add_comm c a, add_comm c b]
   exact add_lt_left h c
 
@@ -61,6 +61,28 @@ theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by
 theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
   rw [add_comm c a, add_comm c b, add_lt_left_iff]
 
+theorem hmul_pos_iff {k : Nat} {a : M} (h : 0 < a) : 0 < k * a ↔ 0 < k:= by
+  rw [← hmul_lt_hmul_iff k h, hmul_zero]
+
+theorem hmul_nonneg {k : Nat} {a : M} (h : 0 ≤ a) : 0 ≤ k * a := by
+  have := hmul_le_hmul (k := k) h
+  rwa [hmul_zero] at this
+
+theorem hmul_le_hmul_of_le_of_le_of_nonneg
+    {k₁ k₂ : Nat} {x y : M} (hk : k₁ ≤ k₂) (h : x ≤ y) (w : 0 ≤ x) :
+    k₁ * x ≤ k₂ * y := by
+  apply Preorder.le_trans
+  · change k₁ * x ≤ k₂ * x
+    obtain ⟨k', rfl⟩ := Nat.exists_eq_add_of_le hk
+    rw [add_hmul]
+    conv => lhs; rw [← add_zero (k₁ * x)]
+    rw [← add_le_right_iff]
+    exact hmul_nonneg w
+  · exact hmul_le_hmul h
+
+theorem add_le_add {a b c d : M} (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d :=
+  Preorder.le_trans (add_le_right a hcd) (add_le_left hab d)
+
 end NatModule.IsOrdered
 
 namespace IntModule.IsOrdered
@@ -138,8 +160,8 @@ theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
 theorem sub_nonneg_iff {a b : M} : 0 ≤ a - b ↔ b ≤ a := by
   rw [add_le_left_iff b, zero_add, sub_add_cancel]
 
-theorem hmul_neg (k : Int) {a : M} (h : a < 0) : 0 < k ↔ k * a < 0 := by
-  simpa [IntModule.hmul_neg, neg_pos_iff] using hmul_pos k (neg_pos_iff.mpr h)
+theorem hmul_neg_iff (k : Int) {a : M} (h : a < 0) : k * a < 0 ↔ 0 < k := by
+  simpa [IntModule.hmul_neg, neg_pos_iff] using hmul_pos_iff k (neg_pos_iff.mpr h)
 
 theorem hmul_nonpos {k : Int} {a : M} (hk : 0 ≤ k) (ha : a ≤ 0) : k * a ≤ 0 := by
   simpa [IntModule.hmul_neg, neg_nonneg_iff] using hmul_nonneg hk (neg_nonneg_iff.mpr ha)