omega fails on Finset.filter cards that print differently but are equal

If one hypothesis has #(C.filter (· ∈ A)) elaborated from an explicit term and another comes from unification (e.g. hAcup _ ... (hCup.mono (filter_subset _ _))), they can elaborate to filter (Membership.mem A) C vs {x ∈ C | x ∈ A}. omega then treats them as different atoms and reports a bogus counterexample. Fix: pass the set explicitly (hAcup (C.filter (· ∈ A)) ... or (C := C.filter (· ∈ B'))) so both sides share one syntactic form. A similar effect: after set m := (L - 1) / k, facts from Nat.div_mul_le_self still mention (L-1)/k; use clear_value/generalize ... = m at h1 h2 before omega.