refine eq_of_indep_iff_indep_forall rfl (fun I hI ↦ ?_)
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
⊢ M ↾ X = loopyOn X
α : 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