simp only [restrict_indep_iff, loopyOn_indep_iff]
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ (M ↾ X).Indep I ↔ (loopyOn X).Indep I
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ M.Indep I ∧ I ⊆ X ↔ I = ∅