simp only [restrict_ground_eq, restrict_indep_iff, freeOn_indep_iff, and_iff_right_iff_imp]
α : 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
α : 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
⊢ J ⊆ I → M.Indep J