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

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f : α
heE : e ∈ M.E
he : ¬M.Coloop e
hf : f ∉ M.E
⊢ M' = M.seriesExtend e f ↔ M'.Series e f ∧ M' ／ f = M
Tactic:
rw [seriesExtend, eq_dual_comm, eq_comm, eq_parallelExtend_iff _ (show f ∉ M✶.E from hf),
  deleteElem, ← contract_dual_eq_dual_delete, ← contract_elem, dual_inj, Series]
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f : α
heE : e ∈ M.E
he : ¬M.Coloop e
hf : f ∉ M.E
⊢ M✶.Nonloop e

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f : α
heE : e ∈ M.E
he : ¬M.Coloop e
hf : f ∉ M.E
⊢ M✶.Nonloop e
Tactic:
rwa [Nonloop, and_iff_left (show e ∈ M✶.E from heE), dual_loop_iff_coloop]
State after:
no goals