rw [Series, seriesExtend, dual_dual]
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ (M.seriesExtend e f).Series e f
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ (M✶.parallelExtend e f).Parallel e f