rw [← relRank_cl_right, eq_comm, ← relRank_cl_right, cl_inter_ground]
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X (Y ∩ M.E) = M.relRank X Y
no goals