refine ⟨fun h ↦ ⟨⟨h.flat_right, ?_⟩,h.subset <| M.mem_cl_self e⟩,
  fun ⟨hL, heL⟩ ↦ by 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
⊢ M.cl {e} ⋖[M] L ↔ M.Line L ∧ e ∈ 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 : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ M.er L = 2