obtain ⟨J, hJ⟩ := M.exists_basis' X
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
case refine'_1.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
J : Set α
hJ : M.Basis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n