simpa [cl_insert_cl_eq_cl_insert, he] using
  (M.cl_flat _).covBy_cl_insert (not_mem_cl_diff_of_mem hI he) (hI.subset_ground 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 : α
hI : M.Indep I
he : e ∈ I
⊢ M.cl (I \ {e}) ⋖[M] M.cl I
no goals