omega and `set`: whole-atom abbreviations are seen through, nested ones are not

Tested on Lean v4.35.0 + Mathlib v4.35.0. After set q := Fintype.card F with hq (or set q := s.card), suppose a later have reintroduces the unfolded term. omega still identifies q with the unfolded term when q is the whole atom: an older q * 2 = 6 (rewritten by set) and a new Fintype.card F + 1 = 5 give False directly. It does NOT when the abbreviation sits inside a larger atom. Older q * x = 6 and new Fintype.card F * x + 1 = 8 give a bogus counterexample. So do set B := s.image f with a new (s.image f ∪ t).card = 7 next to (B ∪ t).card = 8. Fix: rw [← hq] at h_new (clear_value was not needed), or generalize Fintype.card F = q at h1 h2 once all the hypotheses exist. When omega's counterexample lists two atoms that differ only by an abbreviation, this is the cause.