fix: proof construction in grind ring

This PR fixes a bug during proof construction in `grind`.

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -383,7 +383,7 @@ private structure NormResult where
   vars : Array Expr
 
 private def norm (vars : PArray Expr) (lhs rhs lhs' rhs' : RingExpr) : NormResult :=
-  let usedVars     := lhs.collectVars >> lhs.collectVars >> lhs'.collectVars >> rhs'.collectVars <| {}
+  let usedVars     := lhs.collectVars >> rhs.collectVars >> lhs'.collectVars >> rhs'.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
   let vars         := vars'.map fun x => vars[x]!

tests/lean/run/grind_ring_norm_ring_proof.lean

@@ -0,0 +1,5 @@
+example [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α] (a b c : α) :
+  (if a - b ≤ -(a - b) then -(a - b) else a - b) ≤
+  ((if a - c ≤ -(a - c) then -(a - c) else a - c) + if c - d ≤ -(c - d) then -(c - d) else c - d) +
+    if b - d ≤ -(b - d) then -(b - d) else b - d := by
+  split <;> split <;> split <;> split <;> grind