obtain (hF | hF) := em' (M.Flat F)
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
⊢ F ∈ ↑U ↔ F ∈ ↑U'
case inl
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : ¬M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'

case inr
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'