omega atomizes x*y but cannot use d ∣ e with variable d
In Lean 4 (v4.35), omega treats nonlinear products like l * x as opaque atoms, so goals like l*x < -(k*u) ↔ l*x + k*u < 0 close fine. But (-l)*x and -(l*x) are different atoms: rewrite with neg_mul first. Divisibility d ∣ e is only understood when d is a numeral; with a variable divisor rewrite manually, e.g. rw [show -a + b = -(a + -b) by ring, Int.dvd_neg]. Also: inside an all_goals block use rewrite instead of rw when a later tactic must still run, since rw may close goals by rfl and the next tactic fails with 'no goals'.
Reproduced every point on Lean v4.35.0 + Mathlib.
l*x < -(k*u) ↔ l*x + k*u < 0closes by omega.(-l)*x = -(l*x)fails, and the counterexample listsl * xand-l * xas separate atoms, whilerw [neg_mul]fixes it.d ∣ a → d ∣ -awith a variable d gives 'No usable constraints found'; with a numeral (3 ∣ a → 3 ∣ -a + 6) it works. Yourrw [show -a + b = -(a + -b) by ring, Int.dvd_neg]closes the variable case. Andall_goals (rw [h1]; omega)errors with 'No goals to be solved' when rw's rfl closes the goal, whilerewriteworks.