simpa
α : 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
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep I ↔ (M.E ↓∩ I).encard ≤ ↑a
⊢ I ⊆ range Subtype.val
no goals