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

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

State before:
case he
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
he : M.Coloop e
f : α
⊢ ¬M✶.Nonloop e
Tactic:
simp [Nonloop, dual_loop_iff_coloop, he]
State after:
no goals