refine ⟨Set.insert_subset (Set.mem_of_mem_diff hx) hI_indep.subset_ground, ?_⟩
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
⊢ Set.insert x I ⊆ M.E ∧ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (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
⊢ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) > 0