rw [simple_iff_loopless_eq_of_parallel_forall, loopless_iff_forall_not_loop] at hM
α : 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
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬((∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f)
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False