simp_rw [hF₀.covBy_iff_eq_cl_insert]
α : 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₀
he : e ∈ M.E \ F₀
⊢ ∃! F₁, e ∈ F₁ ∧ (F₀ ⋖[M] F₁)
α : 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₀
he : e ∈ M.E \ F₀
⊢ ∃! F₁, e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)