obtain (hU | ⟨F, hF⟩) := (U : Set (Set α)).eq_empty_or_nonempty
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
⊢ U = ⊥ ∨ M.E ∈ U
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
⊢ U = ⊥ ∨ M.E ∈ U

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