rw [simple_iff_loopless_eq_of_parallel_forall, loopless_iff_forall_not_loop]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ M.Simple
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ (∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f