rw [coloop_iff_diff_cl, not_iff_not]
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Coloop e ↔ e ∉ M.cl (M.E \ {e})
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
⊢ M.cl (M.E \ {e}) = M.E ↔ e ∈ M.cl (M.E \ {e})