refine M.indep_iff'.mpr ⟨rIJ.trans hJ.subset_ground, fun x hx ↦ ?_⟩
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hJ : M.Indep J
rIJ : I ⊆ J
⊢ M.Indep I
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hJ : M.Indep J
rIJ : I ⊆ J
x : α
hx : x ∈ I
⊢ M.relRank (I \ {x}) I > 0