rw [flat_deleteElem_iff, and_assoc, and_congr_right_iff]
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (M ＼ e).Flat F ∧ e ∈ M.cl F ↔ e ∉ F ∧ M.cl F = insert e F
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F → ((M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F ↔ M.cl F = insert e F)