obtain ⟨R, hR, rfl⟩ := hM'M.exists_eq_restrict
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
M' : Matroid α
h : N.IsSimplification M
hNM' : N ≤r M'
hM'M : M' ≤r M
⊢ N.IsSimplification M'
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
⊢ N.IsSimplification (M ↾ R)