rw [← relRank_cl_left, ← hI.cl_eq_cl, relRank_cl_left, ← relRank_cl_right, ← hJ.cl_eq_cl,
  relRank_cl_right, hJ.indep.relRank_of_subset hIJ]
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.relRank X Y = (J \ I).encard
no goals