Theorem: Matroid.seriesExtend_contract_eq' (Matroid/Constructions/ParallelExtension.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
⊢ M.seriesExtend e f ／ f = M ／ f
Tactic:
rw [seriesExtend, contract_elem, ← delete_dual_eq_dual_contract, ← deleteElem,
  parallelExtend_delete_eq']
State after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
⊢ (M✶ ＼ f)✶ = M ／ f

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
⊢ (M✶ ＼ f)✶ = M ／ f
Tactic:
simp
State after:
no goals