refine
  covBy_iff.2 ⟨hF₀, M.cl_flat _, (M.subset_cl_of_subset (subset_insert _ _) ?_).ssubset_of_ne ?_,
    fun F hF hF₀F hFF₁ ↦ ?_⟩
case refine_2.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 : α
heF₀ : e ∈ M.E \ F₀
⊢ F₀ ⋖[M] M.cl (insert e F₀)
case refine_2.intro.intro.refine_1
α : 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 : α
heF₀ : e ∈ M.E \ F₀
⊢ insert e F₀ ⊆ M.E

case refine_2.intro.intro.refine_2
α : 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 : α
heF₀ : e ∈ M.E \ F₀
⊢ F₀ ≠ M.cl (insert e F₀)

case refine_2.intro.intro.refine_3
α : 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 : α
heF₀ : e ∈ M.E \ F₀
F : Set α
hF : M.Flat F
hF₀F : F₀ ⊆ F
hFF₁ : F ⊆ M.cl (insert e F₀)
⊢ F = F₀ ∨ F = M.cl (insert e F₀)