simp [hx, hxI, hxe]
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
⊢ x ∈ M.E \ insert e I
no goals