exact U.cl_superset_mem' h (insert_subset hx hss)
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
h : M.cl (insert x (I \ {e})) ∈ U
⊢ M.cl (X \ {e}) ∈ U
no goals