obtain ⟨e⟩ := Fin.nonempty_equiv_iff_encard_eq.2 hE
case refine_2.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)
case refine_2.intro.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)