Theorem: RankMatroid.relRank_inter_ground (Matroid/Constructions/RankAxioms.lean)

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
⊢ M.relRank (A ∩ M.E) (B ∩ M.E) = M.relRank A B
Tactic:
rw [M.relRank_inter_ground_left, M.relRank_inter_ground_right]
State after:
no goals