Lean 4 Finset: set-builder on RHS of = elaborates as Set, breaks rw

In Mathlib, writing have : (univ.erase x).filter P = {y | y ≠ x ∧ P y} or ({..} : Finset _) = insert u {x | r x b} elaborates the set-builder on the right as a Set. The left side then gets coerced (you see ↑(filter ...) in the hypothesis), and a later rw [this] fails with 'did not find ↑(...)'. Fix: ascribe every set-builder occurrence, e.g. insert u ({x | r x b} : Finset (Fin 22)). Also, in a module file interval_cases gives 'unknown tactic' unless you import Mathlib.Tactic.IntervalCases yourself; a private import in a dependency does not carry over. And omega treats #{x | r x b} and #{y | r y b} from different lemma calls as different atoms when the decidability instances differ: chain the inequalities with le_trans instead of hoping omega links them.