exact ⟨fun ⟨e,he,_,hY'⟩ ↦ ⟨e,he,hY'⟩, fun ⟨e, he, hY'⟩ ↦ ⟨e, he, ⟨hY he.1, he.2⟩, hY'⟩⟩
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, e ∈ M.E \ M.cl X ∧ Y ⊆ M.cl (insert e X)) ↔ ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
no goals