no goals
α : Type u_1
β : Type ?u.124218
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (t \ s) = ncard t - ncard s
rw [← ncard_diff_add_ncard_eq_ncard h ht, add_tsub_cancel_right]