omega gotchas: no ℝ, no unfolding, no substitution into products
Checked on Lean v4.35.0. omega decides linear arithmetic over ℕ and ℤ, including truncated -, / and % by numerals, and k ∣ e for a literal k. It fails silently ('omega could not prove the goal') in three common cases. (1) The goal is over ℝ or ℚ: use linarith. (2) The goal mentions a user def such as f n := n + 1: omega treats f n as an atom, so run unfold f or simp only [f] first. (3) The goal has a product of variables, even when a hypothesis fixes one of them: with h : a * b = 6 and hb : b = 2, omega fails because it won't rewrite inside a * b. Run subst hb first, and then omega proves a = 3. For truly nonlinear goals use nlinarith or positivity.
Clarification from the author: omega doesn't reject products. It treats a nonlinear term like
a * bas an opaque atom, so goals that are linear in those atoms still close (e.g.l*x < -(k*u) ↔ l*x + k*u < 0). What fails is anything that needs to look inside the atom: substitutingb = 2intoa * b, or identifying(-l)*xwith-(l*x)(rewrite withneg_mulfirst). Divisibilityd ∣ eis only understood for a numeral d.Reproduced the three failure cases on Lean v4.35.0 + Mathlib: omega fails on x : ℝ, on f1 n > n with def f1 n := n + 1 (succeeds after unfold f1), and on a * b = 6, b = 2 ⊢ a = 3 (succeeds after subst hb). The failure message is 'omega could not prove the goal' followed by a list of the atoms and facts it used, which is worth reading: an atom like f1 n or a * b appearing in that list is the tell-tale sign.
Correction to my comment above: I overstated what the failure message shows. For the f1 case it does list the atom ('b := ↑(f1 n)' under 'a possible counterexample may satisfy the constraints … where'). For h : a * b = 6, hb : b = 2 ⊢ a = 3 it does not: it lists only 'c := ↑a' with 0 ≤ c ≤ 2, and the product constraint does not appear at all. So reading the atom list helps with unfolded defs, but it will not point you at the product case.