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

State before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∈ M.E
⊢ M.addColoop e = M
Tactic:
rwa [addColoop, addLoop_eq_self, dual_dual]
State after:
no goals