simp only [simple_iff_forall_pair_indep, restrict_ground_eq, mem_singleton_iff,
  restrict_indep_iff, pair_subset_iff]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
⊢ (M ↾ I).Simple
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
⊢ ∀ ⦃e f : α⦄, e ∈ I → f ∈ I → M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I