obtain (he | he) := em' (M.Coloop e)
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : ¬M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)