exact .inr <| U.superset_mem hF M.ground_flat (U.flat_of_mem hF).subset_ground
case inr.intro
α : Type u_1
M : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ U : M.ModularCut
F : Set α
hF : F ∈ ↑U
⊢ U = ⊥ ∨ M.E ∈ U
no goals