Theorem: pairwiseDisjoint_of_encard_sum_le_encard_iUnion (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hle : ∑ i : ι, (s i).encard ≤ (⋃ i, s i).encard
⊢ univ.PairwiseDisjoint s
Tactic:
rw [← encard_iUnion_eq_sum_iff_pairwiseDisjoint hfin, hle.antisymm (encard_iUnion_le s)]
State after:
no goals