exact ⟨_, hYne.some_mem, hY'.trans (M.cl_subset_cl (subset_insert _ _))⟩
case refine_1.inr
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
hY' : Y ⊆ M.cl X
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
no goals