refine eq_of_indep_iff_indep_forall rfl (fun J _ ↦ ?_)
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
hI : M.Indep I
⊢ M ↾ I = freeOn I
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R B X Y Z K E : Set α
hI : M.Indep I
J : Set α
x✝ : J ⊆ (M ↾ I).E
⊢ (M ↾ I).Indep J ↔ (freeOn I).Indep J