obtain ⟨I', hI'_indep, hI', hI'_ssubset⟩ := hr hI_indep hI
case refine_2
α : 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
⊢ M.relRank I X ≠ 0
case refine_2.intro.intro.intro
α : 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' ∧ ¬I' ⊆ I
⊢ M.relRank I X ≠ 0