exact ⟨R, hRM', by rw [restrict_restrict_eq _ (show R ⊆ R' from hRM')]⟩
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'
no goals