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