convert congr_arg ((↑) : ℕ → ℕ∞) h_eq
case inr.refine_2
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
⊢ ↑⋯.toFinset.card = ∑ x : ι, ↑⋯.toFinset.card
case h.e'_2.h.e'_3.h.e'_2
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
⊢ ⋯.toFinset = Finset.univ.biUnion fun i => ⋯.toFinset

case h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
h_eq : (Finset.univ.biUnion fun i => ⋯.toFinset).card = ∑ u : ι, ⋯.toFinset.card
⊢ ∑ x : ι, ↑⋯.toFinset.card = ↑(∑ u : ι, ⋯.toFinset.card)