rw [← cl_inter_ground, ← hI.cl_eq_cl] at heX
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I✝ X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
I : Set α
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I✝ X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X