Theorem: Matroid.Connected.loopless (Matroid/Connectivity.lean)

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

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
hE : M.E.Nontrivial
⊢ ∀ e ∈ M.E, ¬M.Loop e
Tactic:
exact fun e _ hl ↦ hl.not_connected hE hM
State after:
no goals