exact M.subset_cl _ (by aesop_mat) hf
α : 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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ f ∈ M.cl (Y ∩ M.E)
no goals