set A := I
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
hJ : M.relRank (J \ {x}) J > 0
⊢ M.relRank (I \ {x}) I > 0
α : Type u_1
A✝ B I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
hJ : M.relRank (J \ {x}) J > 0
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
⊢ M.relRank (A \ {x}) A > 0