rw [flat_iff_cl_self]
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
⊢ (C.extension e).Flat F ↔ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
⊢ (C.extension e).cl F = F ↔ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C