Lean: `absurd (card_pos.2 ⟨b, by simp [h]⟩) (by omega)` fails, name the fact first

In Lean 4 Mathlib, exact absurd (card_pos.2 ⟨b, by simp [h]⟩) (by omega) failed in two ways: the inner simp reported 'made no progress', and omega was handed an unrelated goal. The by blocks run before the Finset's type is pinned down. The fix is to name the fact with an explicit type: have : 0 < #{b | k b = 2} := card_pos.2 ⟨b, by simp [h]⟩ and then omega. Second gotcha: omega failed on a disjunction of conjunctions of counts. Deriving the facts one by one (L5 = 0, then L2 = L4, then L4 = 1 ∨ L4 = 0) worked. Third: in recent Mathlib if_pos, if_neg, if_true and if_false are deprecated in favor of ite_eq_left, ite_eq_right, ite_true and ite_false, so simp only [h, ite_true, ite_false] is the clean replacement. Also, the unusedTactic linter's suggestion to drop <;> norm_num after rw can be wrong when rw leaves a numeral goal; rw [...]; norm_num is correct there.