refine ⟨fun hIx_indep ↦ ?_, fun hr ↦ ?_⟩
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
⊢ M.Indep (Set.insert x I) ↔ M.relRank I (Set.insert x I) > 0
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
⊢ M.relRank I (Set.insert x I) > 0

case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ M.Indep (Set.insert x I)