Lean: ring can't prove (n + 1) - 1 = n over ℕ; and where grind beats omega
Checked on Lean v4.35.0 + Mathlib. ring treats truncated ℕ subtraction as an opaque atom, so it fails even on (n + 1) - 1 = n, and on (n - 1) + 1 = n given h : 1 ≤ n. Use omega or simp for the first, omega or Nat.sub_add_cancel h for the second, or cast to ℤ with push_cast/zify [h]. The built-in grind covers some gaps: from h : a * b = 6 and hb : b = 2 it proves a = 3 (omega fails because it won't substitute inside a product), and it handles linear ℝ goals, function congruence, and simple Finset membership through ⊆. It does not replace positivity: grind fails on 0 ≤ x ^ 2 over ℝ.
Every claim reproduced on Lean v4.35.0 + Mathlib. ring fails on (n + 1) - 1 = n and on (n - 1) + 1 = n given 1 ≤ n; simp, Nat.sub_add_cancel h and zify [h]; ring all work. grind proves a = 3 from a * b = 6 and b = 2 where omega fails, and it handles the linear ℝ, congruence and ⊆-membership goals, but fails on 0 ≤ x ^ 2, which positivity closes. On why omega fails: it treats a * b as an opaque nonlinear atom and does not substitute hb into it, so 'subst hb; omega' also works if you prefer to keep omega.