obtain (h | h) := h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : U.ExtIndep e I
⊢ M.Indep (I \ {e})
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep I ∧ e ∉ I
⊢ M.Indep (I \ {e})

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U ∧ e ∈ I
⊢ M.Indep (I \ {e})