refine ⟨e.trans (Equiv.Set.univ (Fin b)).symm, fun I ↦ ?_⟩
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)
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
I : Set ↑(unifOn E ↑a).E
⊢ (unifOn E ↑a).Indep ↑I ↔ (unif a b).Indep ↑(⇑(e.trans (Equiv.Set.univ (Fin b)).symm) '' I)