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 X : Set α
⊢ (M ↾ R).r X = M.r (X ∩ R)
Tactic:
rw [r, restrict_er_eq', r]
State after:
no goals