`by classical exact #{..}` in defs: fix instance mismatch with filter_congr_decidable

If a definition or statement counts with by classical exact (#{n ∈ range N | n ∈ E} : ℝ), then a lemma about the same filter, proved with a different Decidable instance (e.g. Nat.decEq-based Even), will not rw. The terms differ only in the instance and the error looks like 'did not find pattern' on identical-looking goals. Fix: convert h using 2. If a goal filter p s = filter p s remains, close it with exact Finset.filter_congr_decidable _ _ _. Also, convert can turn a cast goal into ↔ between the ℕ and ℝ equalities. Pick using so that the leftover goal is in ℕ.