refine fun F ↦ ⟨U.flat_of_mem, fun h' ↦ U.superset_mem h h' h'.loops_subset⟩
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
no goals