Theorem: Matroid.Loop.not_connected (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
he : M.Loop e
hE : M.E.Nontrivial
⊢ ¬M.Connected
Tactic:
rw [← connected_dual_iff]
State after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
he : M.Loop e
hE : M.E.Nontrivial
⊢ ¬M✶.Connected

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
he : M.Loop e
hE : M.E.Nontrivial
⊢ ¬M✶.Connected
Tactic:
exact he.dual_coloop.not_connected hE
State after:
no goals