simp only [unifOn_indep_iff, Subtype.val_injective.encard_image, image_subset_iff, unif_ground_eq,
  Equiv.Set.univ, Equiv.trans_apply, Equiv.coe_fn_symm_mk, unif_indep_iff]
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)
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
⊢ I.encard ≤ ↑a ∧ I ⊆ Subtype.val ⁻¹' E ↔ ((fun a_1 => ⟨e a_1, trivial⟩) '' I).encard ≤ ↑a