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

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f x : α
I C : Set α
M : Matroid α
e : α
⊢ M.parallelExtend e e = M.addLoop e
Tactic:
change comap _ (update id e (id e)) ↾ _ = _
State after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f x : α
I C : Set α
M : Matroid α
e : α
⊢ M.comap (update id e (id e)) ↾ insert e M.E = M.addLoop e

State before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f x : α
I C : Set α
M : Matroid α
e : α
⊢ M.comap (update id e (id e)) ↾ insert e M.E = M.addLoop e
Tactic:
rw [update_eq_self, comap_id, addLoop]
State after:
no goals