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 _ _)]
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ (M.addLoop e).Loop e
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ ¬M.Indep {e}