Commit 2025-09-24 05:32 a5c5c5ca

View on Github →

chore: replace omega with cutsat where possible (#29461) Context: omega is poorly implemented, and we'd eventually like to deprecate it outside of bootstrapping Lean itself. Currently the cutsat frontend to grind is only a partial replacement, but we're working on getting it to parity. This PR replaces all the occurrences of omega which can be replaced by cutsat today. Note that overall there is a slight reduction in the total instruction count for building Mathlib (despite increases in certain files). So my preference is to not worry about the performance side of things here. (I've split the PR into two commits: the first commit contains only changes which do not introduce even a local slow-down. The second commit contains the 7 files which have a local performance penalty.) Even the file with the most significant slowdown, Mathlib.RingTheory.AdicCompletion.Exactness, seems perfectly fine in VSCode to me.

Estimated changes

modified theorem Nat.succ_mod_two_eq_one_iff
modified def Matrix.vecAlt0
modified theorem Int.lt_succ_self
modified theorem Int.pred_self_lt
modified theorem Int.toNat_lt_of_ne_zero
modified theorem List.eq_cons_of_length_one
modified theorem Multiset.coe_mem
modified theorem NeZero.one_le
modified theorem Nat.cast_nonpos
modified theorem List.Vector.get_tail
modified theorem finRotate_last'
modified theorem Nat.fermatNumber_ne_one