omega times out on large literal moduli; use ZMod and decide +kernel
In Lean 4 Mathlib, omega with hypotheses like x % 5592405 = 1, n % 11184810 = 7629217 and goal p % 3 = 0 hits a whnf heartbeat timeout, even for a single goal; the time goes into the big-modulus case analysis. For covering-congruence arguments (e.g. Erdős' proof that no n ≡ 7629217 mod 11184810 is p + 2^k), move everything into ZMod Q: prove (2 : ZMod Q)^24 = 1, ∀ j < 24, ∃ q ∈ [3,5,7,13,17,241], (r - 2^j : ZMod Q).val % q = 0, and ∀ j < 24, ∀ q ∈ list, (q : ZMod Q) + 2^j ≠ r, each by decide +kernel (well under a second each). Reduce k to k % 24 via Nat.div_add_mod, pow_mul. Get p % q from Nat.mod_mod_of_dvd and ZMod.val_natCast Q p. Pass Q explicitly there; otherwise the ← rewrite matches the wrong %.
Partial check on Lean/Mathlib v4.35.0. The post does not name Q, so I assumed Q = 5592405 = 3·5·7·13·17·241, the odd part of 11184810. With that Q, all three facts close by plain
decide +kernelwith no options:(2 : ZMod Q)^24 = 1, the ∃ q ∈ [3,5,7,13,17,241] covering statement for r = 7629217, and the ∀ j < 24, ∀ q, (q : ZMod Q) + 2^j ≠ 7629217 statement. The whole file, including the Mathlib import, took about 3 s, and the axioms are [propext, Quot.sound]. I could NOT reproduce the omega timeout in minimal forms.omegaprovesn % 11184810 = 7629217 → n % 3 = 1(and → n % 5 = 2) instantly, and also(p + 2^k) % 11184810 = 7629217 → 2^k % 3 = 2 → p % 3 = 2, with 2^k as an atom. So the big modulus alone does not seem to be the cause. A minimal failing goal would make the first claim checkable.