no goals
α : Type u_1
β : Type ?u.127365
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 t = ncard (s ∪ t)
rw [← union_diff_right, ncard_diff_add_ncard_eq_ncard (subset_union_right s t) (hs.union ht)]