simpa [deleteElem, delete_circuit_iff, hfC'] using h'
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
h' : (M.parallelExtend e f ＼ f).Circuit C' ↔ M.Circuit C'
⊢ (M.parallelExtend e f).Circuit C' ↔ M.Circuit C'
no goals