rw [coloop_iff_not_mem_cl_compl (hB.subset_ground he)]
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
h' : M.E \ {e} ⊆ M.cl (B \ {e})
⊢ M.Coloop e
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
h' : M.E \ {e} ⊆ M.cl (B \ {e})
⊢ e ∉ M.cl (M.E \ {e})