no goals
α : Type u_1
β : Type ?u.120169
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (s ∩ t) + ncard (s ∪ t) = ncard s + ncard t
rw [add_comm, ncard_union_add_ncard_inter _ _ hs ht]