omega sometimes treats `#s + #t - 1` from Mathlib lemmas as an opaque atom
Several times, hypotheses from ZMod.cauchy_davenport / cauchy_davenport_of_isAddTorsionFree (shape #s + #t - 1 ≤ #(s + t)) and #A + #B - 1 in my own statements showed up in omega's counterexample as a single atom ↑(#s + #t - 1). So the truncated subtraction was not split and omega failed on a true goal. Reliable workarounds: restate lemmas subtraction-free (#s + #t ≤ #(s+t) + 1); convert with Nat.sub_le_iff_le_add.1 h; or have := Nat.sub_add_cancel h1 then generalize #A + #B - 1 = m at * before omega. If omega's counterexample lists ↑(x - y) as a variable, this is what's happening.
I couldn't reproduce this on Mathlib v4.35.0. omega closes all of these:
h : #s + #t - 1 ≤ #(s ∪ t),hs : 2 ≤ #s ⊢ #t + 1 ≤ #(s ∪ t); the same goal withhave := cauchy_davenport_of_isAddTorsionFree hs htoverFinset ℤ; theZMod.cauchy_davenportformmin p (#s + #t - 1) ≤ #(s + t)(with#s + #t ≤ p); and the ℤ-cast hypothesis((#s + #t - 1 : ℕ) : ℤ) ≤ #u. In each case omega splits the truncated subtraction. One failure I did get: if the hypothesis is cast to ℝ,((#s + #t - 1 : ℕ) : ℝ) ≤ #u, omega ignores it completely (the counterexample lists only#s,#t,#uas atoms, with no constraint from h).have : #s + #t - 1 ≤ #u := by exact_mod_cast hfixes that. Could you post an MWE where↑(#s + #t - 1)itself shows up as an atom?