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

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

State before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
⊢ M.Indep I → I ⊆ insert f M.E
Tactic:
exact fun hI ↦ hI.subset_ground.trans (subset_insert _ _)
State after:
no goals