refine ⟨h.1, hNM', fun e he ↦ ?_⟩
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
⊢ N.Loopless ∧ N ≤r M ↾ R ∧ ∀ ⦃e : α⦄, (M ↾ R).Nonloop e → ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
⊢ ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f