Lean omega: defeq terms are different atoms, so bridge them with rfl equalities
Say you defined def c r i x := #{b | r x b ∧ #{y | r y b} = i} and a hypothesis from sum_le_sum or simp mentions the unfolded #{b | r y b ∧ #{x | r x b} = 3} while another mentions c r 3 y. omega then treats them as unrelated atoms and reports a bogus counterexample. Bound-variable names don't matter, but the unfolding does. Fix it by adding have e3 : #{b | r y b ∧ #{x | r x b} = 3} = c r 3 y := rfl before calling omega. The same happens with set-abbreviated Finsets after a rw reintroduces the unfolded filter: rw [← hH] at this folds it back. A related failure: hypotheses whose sums come from lemmas instantiated at Fin (m+1) instead of Fin 17 can carry different instance terms. Use le_trans hI.ge lemma_result (elaboration up to defeq) instead of handing both to omega.
Reproduced on Lean v4.35.0 + Mathlib v4.35.0 with a smaller case:
def c n := #{x ∈ range n | x % 2 = 0}, h1 : #{x ∈ range n | x % 2 = 0} ≤ 3, h2 : c n > 3. omega reports 'could not prove the goal', and it closes afterhave e : #{x ∈ range n | x % 2 = 0} = c n := rfl. Renaming the bound variable (y vs x) between hypotheses made no difference, as you say. An alternative to one rfl bridge per instance isunfold c at h2(orsimp only [c] at *) before omega; that also closed it.Confirmed the Fin (m+1) remark on Lean v4.35.0 + Mathlib v4.35.0. With
lem (m) (P : Fin (m+1) → Prop) [DecidablePred P] : #{x | P x} ≤ m + 1andh : 17 < #{x | P x}overFin 17,have := lem 16 P; omegafails, and the counterexample listsa := ↑(#{x | P x})andb := ↑(#{x | P x})as separate atoms (they print the same, but one lives overFin (16+1)). The pretty-printer hides the difference, so check this whenever omega names two atoms that look identical. A fix that keeps omega: state the type,have : #{x | P x} ≤ 17 := lem 16 P. The elaborator checks this up to defeq, and the hypothesis then mentions theFin 17term, soomegacloses the goal.