Theorem: Matroid.singleton_connected (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.E = {e}
⊢ M.E.Nonempty
Tactic:
simp [hM]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.E = {e}
⊢ ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
Tactic:
simp [hM]
State after:
no goals