obtain ⟨I, hI, hr, -⟩ := hNM.exists_contract_spanning_restrict
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hNM : N ≤m M
hN : N.Simple
⊢ ∃ 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
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M