rwa [← hL.mem_iff_covBy he]
α : 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 : α
he : M.Nonloop e
x✝ : M.Line L ∧ e ∈ L
hL : M.Line L
heL : e ∈ L
⊢ M.cl {e} ⋖[M] L
no goals