rw [deleteElem, flat_delete_iff]
α : 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 : α
⊢ (M ＼ e).Flat F ↔ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert 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 : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) ↔ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))