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

State before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∈ M.E
⊢ M.addLoop e = M
Tactic:
rw [addLoop, insert_eq_of_mem he, restrict_ground_eq_self]
State after:
no goals