exact ⟨e, he, rfl⟩
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ ∃ x, M.Nonloop x ∧ f x = f e
no goals