exact indep_subset hI'_indep (Set.insert_subset hxI' hI'_ssubset.subset)
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
⊢ M.Indep (Set.insert x I)
no goals