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

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ (M.seriesExtend e f).Series e f
Tactic:
rw [Series, seriesExtend, dual_dual]
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ (M✶.parallelExtend e f).Parallel e f

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ (M✶.parallelExtend e f).Parallel e f
Tactic:
apply parallelExtend_parallel
State after:
case he
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ : α
heE : e ∈ M.E
he : ¬M.Coloop e
f : α
⊢ M✶.Nonloop e

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