Theorem: Matroid.relRank_empty_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 ∅ X = M.er X
Tactic:
rw [relRank_eq_er_contract, contract_empty]
State after:
no goals