rw [uniqueBaseOn_base_iff inter_subset_right, and_iff_right rfl]
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).Base (I ∩ E) ∧ (I ∩ E).Finite
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (I ∩ E).Finite