rw [← add_zero (encard (s ∪ t)), ← encard_union_add_encard_inter, WithTop.add_left_cancel_iff
  h.encard_lt_top.ne, encard_eq_zero, disjoint_iff_inter_eq_empty]
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : (s ∪ t).Finite
⊢ s.encard + t.encard = (s ∪ t).encard ↔ Disjoint s t
no goals