simp only [SetLike.ext_iff, mem_top_iff]
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ U = ⊤
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ ∀ (x : Set α), x ∈ U ↔ M.Flat x