simp [hM]
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
⊢ X ⊆ M.E
no goals