rw [← hI.cl_inter_eq_self_of_subset (hIs X hX')]
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ X
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ M.cl X ∩ I