rw [inter_eq_self_of_subset_right hJ]
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.Basis (I ∩ J) J
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.Basis J J