simpa using hIe
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : {e} ⊆ {e} ∩ I
heM : e ∈ M.E
⊢ e ∈ I
no goals