rw [hB.compl_base_dual.cl_eq, dual_ground]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M✶.cl (M.E \ B)
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M.E