obtain ⟨J, hJ⟩ := M.exists_basis I
case mpr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
⊢ M.Indep I
case mpr.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
⊢ M.Indep I