by_contra! h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬M.Simple
⊢ (∃ e, M.Loop e) ∨ ∃ e f, M.Parallel e f ∧ e ≠ f
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬M.Simple
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False