obtain ⟨f, hN⟩ := hN
case intro.intro.inr
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
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}
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E