exact connectedTo_self h.mem_ground_left
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.ConnectedTo e e
⊢ M✶.ConnectedTo e e

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ M✶.ConnectedTo e f
case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ M✶.ConnectedTo e f