refine eq_of_base_iff_base_forall rfl (fun B hBE ↦ ?_)
α : 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 ∅
⊢ M = uniqueBaseOn (M✶.cl ∅) M.E
α : 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