exact hI.subset_cl.trans (M.cl_subset_cl (subset_diff_singleton heIB.2 h.2.2))
case intro.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B✝ C K : Set α
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ X ⊆ M.cl (B \ {e})
no goals