simp [(h x hxI hx.1).1 h'] at hx
α : 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 : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
x : α
hx : x ∈ X \ {e}
h' : M.Indep (insert x I)
hxI : x ∉ I
⊢ False
no goals