rw [diff_singleton_subset_iff]
α : 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 ⊆ insert e F