rw [← singleton_union, union_inter_distrib_right, union_subset_iff,
   (and_iff_left inter_subset_left)]
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : M.Flat F
e : α
he : e ∉ M.E \ F
⊢ insert e F ∩ M.E ⊆ F
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : M.Flat F
e : α
he : e ∉ M.E \ F
⊢ {e} ∩ M.E ⊆ F