no goals
α : Type u_1
β : Type ?u.31550
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ card (s ∪ ∅) + card (s ∩ ∅) = card s + card ∅
simp
no goals
α : Type u_1
β : Type ?u.31550
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : ¬a ∈ r
h : card (s ∪ r) + card (s ∩ r) = card s + card r
⊢ card (s ∪ insert a r) + card (s ∩ insert a r) = card s + card (insert a r)
by_cases a ∈ s <;>
simp [*, ← add_assoc, add_right_comm _ 1]