obtain ⟨e, f, hef, hne⟩ := hM (fun e _ ↦ h.1 e)
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
⊢ False
case intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
e f : α
hef : M.Parallel e f
hne : e ≠ f
⊢ False