have hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E) :=
  (uniqueBaseOn_basis_iff inter_subset_right inter_subset_right).2 rfl
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
I E X : Set α
⊢ (uniqueBaseOn I E).cl X = X ∩ I ∩ E ∪ E \ I
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
⊢ (uniqueBaseOn I E).cl X = X ∩ I ∩ E ∪ E \ I