Theorem: Matroid.relRank_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 : Set α
⊢ M.relRank M.E X = 0
Tactic:
rw [← relRank_inter_ground_right, M.relRank_eq_zero_of_subset inter_subset_right]
State after:
no goals