rw [← cl_insert_cl_eq_cl_insert, ← hI.cl_eq_cl, cl_insert_cl_eq_cl_insert, he.1.mem_cl_iff] at *
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ f ∈ M.cl (insert e (X ∩ M.E))
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ M.Dep (insert f (insert e I)) ∨ f ∈ insert e I