simp only [addLoop, restrict_indep_iff, and_iff_left_iff_imp]
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
⊢ (M.addLoop f).Indep I ↔ M.Indep I
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
⊢ M.Indep I → I ⊆ insert f M.E