rw [seriesExtend, eq_dual_comm, eq_comm, eq_parallelExtend_iff _ (show f ∉ M✶.E from hf),
  deleteElem, ← contract_dual_eq_dual_delete, ← contract_elem, dual_inj, Series]
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f : α
heE : e ∈ M.E
he : ¬M.Coloop e
hf : f ∉ M.E
⊢ M' = M.seriesExtend e f ↔ M'.Series e f ∧ M' ／ f = M
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f : α
heE : e ∈ M.E
he : ¬M.Coloop e
hf : f ∉ M.E
⊢ M✶.Nonloop e