refine ⟨?_, fun ⟨hss, e, he, h⟩ ↦ ⟨e, ?_, h.antisymm ?_⟩⟩
α : 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₀
hF : M.Flat F
⊢ (∃ e ∈ M.E \ F₀, F = M.cl (insert e F₀)) ↔ F₀ ⊆ F ∧ ∃ e ∈ F \ 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₀
hF : M.Flat F
⊢ (∃ e ∈ M.E \ F₀, F = M.cl (insert e F₀)) → F₀ ⊆ F ∧ ∃ e ∈ F \ 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₀
hF : M.Flat F
x✝ : F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)
hss : F₀ ⊆ F
e : α
he : e ∈ F \ F₀
h : F ⊆ M.cl (insert e F₀)
⊢ e ∈ M.E \ F₀

case refine_3
α : 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₀
hF : M.Flat F
x✝ : F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)
hss : F₀ ⊆ F
e : α
he : e ∈ F \ F₀
h : F ⊆ M.cl (insert e F₀)
⊢ M.cl (insert e F₀) ⊆ F