simp only [simple_iff_forall_pair_indep, uniqueBaseOn_ground, uniqueBaseOn_indep_iff',
  subset_inter_iff, pair_subset_iff]
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ (uniqueBaseOn I E).Simple ↔ E ⊆ I
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ (∀ ⦃e f : α⦄, e ∈ E → f ∈ E → (e ∈ I ∧ f ∈ I) ∧ e ∈ E ∧ f ∈ E) ↔ E ⊆ I