rintro ⟨E, rfl, hE⟩
case refine_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) → Nonempty (M ≂ unif a b)
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)