rintro (⟨e, he, hY'⟩ | hY')
case refine_1
α : 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✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X → ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
case refine_1.inl.intro.intro
α : 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✝
e : α
he : e ∈ Y \ M.cl X
hY' : Y ⊆ M.cl (insert e X)
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)

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)