rw [uniqueBaseOn_base_iff (show M✶.cl ∅ ⊆ M.E from M✶.cl_subset_ground _)]
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ (uniqueBaseOn (M✶.cl ∅) M.E).Base B
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ B = M✶.cl ∅