rw [seriesExtend, parallelExtend_not_nonloop, addColoop, deleteElem, contract_elem,
  contract_dual_eq_dual_delete]
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
he : M.Coloop e
f : α
⊢ M.seriesExtend e f = (M ／ f).addColoop f
case he
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
he : M.Coloop e
f : α
⊢ ¬M✶.Nonloop e