rw [contract_dual_eq_dual_delete] at hef
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M ／ C)✶.ConnectedTo e f
⊢ M.ConnectedTo e f
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M✶ ＼ C).ConnectedTo e f
⊢ M.ConnectedTo e f