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