rw [loopless_iff_forall_not_loop]
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
hE : M.E.Nontrivial
⊢ M.Loopless
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
hE : M.E.Nontrivial
⊢ ∀ e ∈ M.E, ¬M.Loop e