rw [parallel_iff_circuit hne]
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ (M ／ (C \ {e, f})).Parallel e f
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ (M ／ (C \ {e, f})).Circuit {e, f}