Theorem: Matroid.seriesExtend_eq_seriesExtend_contract (Matroid/Constructions/ParallelExtension.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
hef : e ≠ f
⊢ M.seriesExtend e f = (M ／ f).seriesExtend e f
Tactic:
rw [seriesExtend, parallelExtend_eq_parallelExtend_delete _ hef, seriesExtend]
State after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
hef : e ≠ f
⊢ ((M✶ ＼ f).parallelExtend e f)✶ = ((M ／ f)✶.parallelExtend e f)✶

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ : α
M : Matroid α
e f : α
hef : e ≠ f
⊢ ((M✶ ＼ f).parallelExtend e f)✶ = ((M ／ f)✶.parallelExtend e f)✶
Tactic:
simp only [deleteElem, contract_elem, contract_dual_eq_dual_delete]
State after:
no goals