push_neg at hM
α : 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
α : 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