no goals
α : Type u_1
β : Type ?u.128103
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (s ∩ t) + ncard (s \ t) = ncard s
simp_rw [← ncard_diff_add_ncard_eq_ncard (diff_subset s t) hs, sdiff_sdiff_right_self,
  inf_eq_inter]