rw [← cl_inter_ground, inter_comm, inter_diff_distrib_left,
  inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, cl_inter_ground]
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
h : ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.cl (I \ {e}) = M.cl I
no goals