exact fun hJU ↦ h.2 <| U.cl_superset_mem' hJU <| diff_subset_diff_left hJI
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hJI : J ⊆ I
heJ : e ∈ J
⊢ M.cl (J \ {e}) ∉ U
no goals