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

State before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
R : Set α
hXR : X ⊆ R
⊢ (M ↾ R).r X = M.r X
Tactic:
rw [r, M.restrict_er_eq hXR, r]
State after:
no goals