refine ⟨fun h x hx heC ↦ (h.not_mem_circuit <| hB.fundCct_circuit hx) heC, fun h ↦ ?_⟩
α : 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
⊢ M.Coloop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
α : 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
⊢ M.Coloop e