exact ⟨e, ⟨(M.cl_subset_ground _) he.1, he.2⟩, rfl⟩
case refine_1.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
h : F₀ ⋖[M] M.cl (insert e F₀)
he : e ∈ M.cl (insert e F₀) \ F₀
⊢ ∃ e_1 ∈ M.E \ F₀, M.cl (insert e F₀) = M.cl (insert e_1 F₀)
no goals