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

State before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ (M.addLoop e).Loop e
Tactic:
rw [addLoop, ← singleton_dep, Dep, singleton_subset_iff, restrict_indep_iff,
  singleton_subset_iff, restrict_ground_eq, and_iff_left (mem_insert _ _),
  and_iff_left (mem_insert _ _)]
State after:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ ¬M.Indep {e}

State before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ ¬M.Indep {e}
Tactic:
exact fun hi ↦ he (singleton_subset_iff.1 hi.subset_ground)
State after:
no goals