unfold Basis
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : J ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X}
⊢ M.Basis J X
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : J ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X}
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ X} ∧ X ⊆ M.E