have hFE := ((subset_insert _ _).trans hF.subset_ground)
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
⊢ M.Flat F
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.Flat F