rw [← hI.not_mem_cl_iff_of_not_mem h]
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I)
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ e ∉ M.cl I