apply subset_antisymm _ (subset_diff_singleton (M.subset_cl _ ((subset_insert _ _).trans
 hF.subset_ground)) e_nF)
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} = F
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} ⊆ F