simp_rw [hF₀.covBy_iff_eq_cl_insert, relRank_eq_one_iff hF.subset_ground, hF₀.cl]
α : 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
⊢ F₀ ⋖[M] F ↔ F₀ ⊆ F ∧ M.relRank F₀ F = 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₀)