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