rw [flat_iff_cl_self, deleteElem, delete_cl_eq, diff_singleton_eq_self e_nF]
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ (M ＼ e).Flat F
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} = F