simpa [(U.flat_of_mem hFU), heF, (U.flat_of_mem hFU).cl]
case mpr.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : F ∈ U
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
no goals