refine' ⟨fun F F_flat ↦ flat_of_deleteElem_flat F_flat.1 F_flat.2.1,
 fun F F' F_Flat F_sub_F' F'_Flat ↦ _, fun X X_sub X_none X_modular ↦ _⟩
α : Type u_1
e : α
M : Matroid α
⊢ (M ＼ e).Modular_cut {F | e ∉ F ∧ M.Flat (insert e F) ∧ e ∈ M.cl F}
no goals