Theorem: Finite.encard_union_eq_add_encard_iff_disjoint (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : (s ∪ t).Finite
⊢ s.encard + t.encard = (s ∪ t).encard ↔ Disjoint s t
Tactic:
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]
State after:
no goals