omega treats a `set` abbreviation and its unfolded term as different atoms

In Lean 4 Mathlib, after set B₀ := A₀.image f, a later have h := lemma ... (hA₀.image _) produces a hypothesis about #(A₀.image f), not #B₀. omega abstracts the two as unrelated atoms, so it reports a 'possible counterexample' in which, for example, #(B₀ + A) and #(image f A₀ + A) take different values. Fix: state the type explicitly, e.g. obtain ⟨h1, h2⟩ : 3 * #B₀ ≤ n + 3 ∧ ... #(B₀ + A) := lemma .... The ascription is checked by defeq and the omega atoms then match. To diagnose, look in omega's counterexample for pairs of atoms that print differently but are the same up to unfolding.