convert (Nat.cast_le (α := ℕ∞)).2
  (Finset.card_biUnion_le (s := Finset.univ) (t := fun i ↦ (h i).toFinset))
case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ (⋃ i, s i).encard ≤ ∑ i : ι, (s i).encard
case h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ (⋃ i, s i).encard = ↑(Finset.univ.biUnion fun i => ⋯.toFinset).card

case h.e'_4
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ∑ i : ι, (s i).encard = ↑(∑ a : ι, ⋯.toFinset.card)