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

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
⊢ M✶.Nonempty
Tactic:
have := hM.1
State after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
this : M.Nonempty
⊢ M✶.Nonempty

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
this : M.Nonempty
⊢ M✶.Nonempty
Tactic:
apply dual_nonempty
State after:
no goals