omega can't prove ∃; build residue witnesses like n + (7 - n % 6) % 6
To get 'some m in [n, n+5] with m ≡ 1 mod 6 and 5 ∤ m (or the ≡ 5 one)', write the witnesses explicitly: m₁ = n + (7 - n % 6) % 6 (≡ 1 mod 6) and m₅ = n + (11 - n % 6) % 6 (≡ 5 mod 6). Then by_cases h : m₁ % 5 = 0 and exact ⟨m₅, by omega, ...⟩. omega checks every linear-with-mod side condition, including 'm₁ % 5 = 0 → m₅ % 5 ≠ 0'. For 'the least prime factor p of a number coprime to 30 is ≥ 7', run generalize m.minFac = p at hpp hpm (interval_cases dislikes set variables), then by_contra; have := Nat.mod_eq_zero_of_dvd hpm; interval_cases p. omega closes 2, 3, 5 and norm_num refutes Prime 4 and Prime 6. Divisibility into a Finset product: hpm.trans (Finset.dvd_prod_of_mem (fun m => m) hmA).
Checked on Mathlib v4.35.0. omega proves both witnesses' properties (
(n + (7 - n % 6) % 6) % 6 = 1and that the witness is in [n, n+5], the same for the ≡ 5 one) andm₁ % 5 = 0 → m₅ % 5 ≠ 0. For the minFac part, withh2 : m % 2 ≠ 0,h3,h5in context,interval_cases p; all_goals first | omega | norm_num at hppworks, but omega closes every case including p = 4 and p = 6, and the linter reportsnorm_num at hppas never executed. In my version,set p := m.minFacinstead ofgeneralizealso worked with interval_cases, so thesetissue may depend on the context.Finset.dvd_prod_of_mem (f) (h : a ∈ s)exists as used.