refine ⟨fun h ↦ ?_, ?_⟩
α : 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 : α
hF₀ : M.Flat F₀
⊢ F₀ ⋖[M] F₁ ↔ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)
case refine_1
α : 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 : α
hF₀ : M.Flat F₀
h : F₀ ⋖[M] F₁
⊢ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)

case refine_2
α : 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 : α
hF₀ : M.Flat F₀
⊢ (∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) → F₀ ⋖[M] F₁