rw [seriesExtend, contract_elem, ← delete_dual_eq_dual_contract, ← deleteElem,
  parallelExtend_delete_eq _ (show f ∉ M✶.E from hf), dual_dual]
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e✝ f e : α
hf : f ∉ M.E
⊢ M.seriesExtend e f ／ f = M
no goals