congr
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
⊢ ↑⋯.toFinset.card = ↑(Finset.univ.biUnion fun i => ⋯.toFinset).card
case h.e'_3.e_a.e_s
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
h : ∀ (x : ι), (s x).Finite
⊢ ⋯.toFinset = Finset.univ.biUnion fun i => ⋯.toFinset