simpa using (hI {x} (by simpa) (finite_singleton _)).subset_ground
case refine_2
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x✝ y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E
no goals