rw [ModularCut.delete, ModularCut.restrict, ModularCut.mem_mk_iff, mem_setOf_eq,
  ← delete_eq_restrict, ← deleteElem, flat_deleteElem_iff]
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ F ∈ U.delete {e} ↔ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl 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))) ∧ M.cl F ∈ U ↔ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)