Theorem: Matroid.modular_cut_of_flats_remove (Matroid/Old/ModularCut.lean)

State before:
α : Type u_1
e : α
M : Matroid α
⊢ (M ＼ e).Modular_cut {F | e ∉ F ∧ M.Flat (insert e F) ∧ e ∈ M.cl F}
Tactic:
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 ↦ _⟩
State after:
no goals