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

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

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