rw [(M.cl_flat {e}).covBy_iff_relRank_eq_one hL.flat, hL.flat.cl_subset_iff_subset,
  singleton_subset_iff, iff_self_and, relRank_cl_left]
α : 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 : α
hL : M.Line L
he : M.Nonloop e
⊢ e ∈ L ↔ M.cl {e} ⋖[M] L
α : 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 : α
hL : M.Line L
he : M.Nonloop e
⊢ e ∈ L → M.relRank {e} L = 1