apply Indep.simple_of_contract_simple (I := I) _ (by rwa [← hN'])
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ (M ↾ (N.E ∪ I)).Simple
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ (M ↾ (N.E ∪ I)).Indep I