have _ := freeOn_rkPos hC
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
⊢ (circuitOn C).Base B ↔ ∃ e ∉ B, insert e B = C
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
x✝ : (freeOn C).RkPos
⊢ (circuitOn C).Base B ↔ ∃ e ∉ B, insert e B = C