rw [hAUB] at hJ
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
hAIB : I \ {x} = I ∩ (J \ {x})
⊢ M.relRank (A \ {x}) A > 0
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B (I ∪ J \ {x}) > 0
hAUB : J = I ∪ J \ {x}
hAIB : I \ {x} = I ∩ (J \ {x})
⊢ M.relRank (A \ {x}) A > 0