no goals
α : Type u_1
β : Type ?u.33976
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : _root_.Disjoint s t
⊢ card (s ∪ t) = card s + card t
rw [← disjUnion_eq_union s t h, card_disjUnion _ _ _]