chore: remove unnecessary hypothesis in ToInt helper theorems

src/Init/Grind/ToIntLemmas.lean

@@ -51,6 +51,10 @@ theorem of_not_lt {α i} [ToInt α i] [_root_.LT α] [ToInt.LT α i] {a b : α}
   intro h; have h' := ToInt.LT.lt_iff a b
   simp [h, h₁, h₂] at h'; assumption
 
+private theorem isNonempty {α i} [ToInt α i] (a : α) : i.nonEmpty = true := by
+  have := ToInt.toInt_mem a; simp; split <;> simp
+  simp at this; omega
+
 /-! Addition -/
 
 theorem add_congr {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] {a b : α} {a' b' : Int}
@@ -61,13 +65,15 @@ theorem add_congr.ww {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i
     (h₁ : toInt a = i.wrap a') (h₂ : toInt b = i.wrap b') : toInt (a + b) = i.wrap (a' + b') := by
   rw [add_congr h₁ h₂, ← i.wrap_add h]
 
-theorem add_congr.wr {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int}
+theorem add_congr.wr {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) {a b : α} {a' b' : Int}
     (h₁ : toInt a = a') (h₂ : toInt b = i.wrap b') : toInt (a + b) = i.wrap (a' + b') := by
+  have h' := isNonempty a
   have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem a)
   rw [h₁] at this; rw [← this] at h₁; apply add_congr.ww h h₁ h₂
 
-theorem add_congr.wl {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int}
+theorem add_congr.wl {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) {a b : α} {a' b' : Int}
     (h₁ : toInt a = i.wrap a') (h₂ : toInt b = b') : toInt (a + b) = i.wrap (a' + b') := by
+  have h' := isNonempty a
   have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem b)
   rw [h₂] at this; rw [← this] at h₂; apply add_congr.ww h h₁ h₂
 
@@ -81,13 +87,15 @@ theorem mul_congr.ww {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i
     (h₁ : toInt a = i.wrap a') (h₂ : toInt b = i.wrap b') : toInt (a * b) = i.wrap (a' * b') := by
   rw [ToInt.Mul.toInt_mul, h₁, h₂, ← i.wrap_mul]; apply h
 
-theorem mul_congr.wr {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int}
+theorem mul_congr.wr {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) {a b : α} {a' b' : Int}
     (h₁ : toInt a = a') (h₂ : toInt b = i.wrap b') : toInt (a * b) = i.wrap (a' * b') := by
+  have h' := isNonempty a
   have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem a)
   rw [h₁] at this; rw [← this] at h₁; apply mul_congr.ww h h₁ h₂
 
-theorem mul_congr.wl {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int}
+theorem mul_congr.wl {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) {a b : α} {a' b' : Int}
     (h₁ : toInt a = i.wrap a') (h₂ : toInt b = b') : toInt (a * b) = i.wrap (a' * b') := by
+  have h' := isNonempty a
   have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem b)
   rw [h₂] at this; rw [← this] at h₂; apply mul_congr.ww h h₁ h₂
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean

@@ -190,12 +190,12 @@ private def mkBinOpThms (opBaseName : Name) (thmName : Name) : ToIntM ToIntThms
     some <| mkApp6 (mkConst cwwName [info.u]) info.type info.rangeExpr info.toIntInst opInst toIntOpInst eagerReflBoolTrue
   else
     none
-  let c_wl? := if info.range.isFinite && info.range.nonEmpty && env.contains cwwName then -- TODO: nonEmpty may be unknown if symbolic bounds
-    some <| mkApp7 (mkConst cwlName [info.u]) info.type info.rangeExpr info.toIntInst opInst toIntOpInst eagerReflBoolTrue eagerReflBoolTrue
+  let c_wl? := if info.range.isFinite && env.contains cwlName then
+    some <| mkApp6 (mkConst cwlName [info.u]) info.type info.rangeExpr info.toIntInst opInst toIntOpInst eagerReflBoolTrue
   else
     none
-  let c_wr? := if info.range.isFinite && info.range.nonEmpty && env.contains cwwName then -- TODO: nonEmpty may be unknown if symbolic bounds
-    some <| mkApp7 (mkConst cwrName [info.u]) info.type info.rangeExpr info.toIntInst opInst toIntOpInst eagerReflBoolTrue eagerReflBoolTrue
+  let c_wr? := if info.range.isFinite && env.contains cwrName then
+    some <| mkApp6 (mkConst cwrName [info.u]) info.type info.rangeExpr info.toIntInst opInst toIntOpInst eagerReflBoolTrue
   else
     none
   return { c? := some c, c_ww?, c_wl?, c_wr? }