rw [hI.cl_eq_cl, hI'.cl_eq_cl]
α : Type u_1
M : Matroid α
B B' I✝ I'✝ J✝ K X✝ Y✝ I I' J J' X Y : Set α
hI : M.Basis' I X
hI' : M.Basis' I' X
hJ : M.Basis' J Y
hJ' : M.Basis' J' Y
⊢ M.cl I = M.cl I'
no goals