no goals
α : Type u_1
β : Type ?u.42409
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ card (filter p s) + card (filter (fun a => ¬p a) s) = card s
classical rw [← card_union_eq (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]
no goals
α : Type u_1
β : Type ?u.42409
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ card (filter p s) + card (filter (fun a => ¬p a) s) = card s
rw [← card_union_eq (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]