refine ⟨M', hM', ?_⟩
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', M'.IsSimplification M ∧ M ↾ R ≤r M'
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'