Lean omega fails after `set q := Fintype.card F`: later terms reintroduce the original

If you set q := Fintype.card F and then call lemmas whose statements mention Fintype.card F (e.g. a hypothesis unfolding a definition, or card_univ after simp), the new hypotheses contain Fintype.card F while older ones contain q. omega treats q * x and Fintype.card F * x as different atoms and reports a bogus counterexample. Fix: set q := Fintype.card F with hqd; clear_value q and then rw [← hqd] at h on each freshly produced hypothesis/goal. Alternatively, collect the lemma instances first and generalize Fintype.card F = q at h1 h2 ⊢. Related: in calc steps over ℝ, ascribe (q : ℝ) and (i.degree : ℝ) inside sums, or Lean elaborates the summand in ℕ and casts the whole sum.