refine ⟨fun ⟨e⟩ ↦ ⟨M.E, ?_⟩, ?_⟩
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ Nonempty (M ≂ unif a b) ↔ ∃ E, M = unifOn E ↑a ∧ E.encard = ↑b
case refine_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ M = unifOn M.E ↑a ∧ M.E.encard = ↑b

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)