have hN' := hr.eq_restrict ▸
  M.contract_restrict_eq_restrict_contract _ _ (subset_diff.1 hr.subset).2.symm
case intro.intro.intro
α : 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
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
case intro.intro.intro
α : 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 ≤m M₀ ∧ M₀.IsSimplification M