Theorem: Matroid.relRank_inter_ground_left (Matroid/Minor/Rank.lean)

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