obtain ⟨R, hR, rfl⟩ := hNM
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
hNM : N ≤r M
⊢ N = M ＼ (M.E \ N.E)
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝¹ B X Y Z K D D₁ D₂ R✝ R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)