have hrw : insert e F ∩ M.E = F := by
  refine subset_antisymm ?_ (subset_inter (subset_insert _ _) hF.subset_ground)
  rw [← singleton_union, union_inter_distrib_right, union_subset_iff,
     (and_iff_left inter_subset_left)]
  rintro f ⟨rfl, hf⟩
  exact by_contra fun hfF ↦ he ⟨hf, hfF⟩
case neg
α : 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
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
case neg
α : 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
hrw : insert e F ∩ M.E = F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F