Theorem: Matroid.delete_elem_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 α
heX : e ∉ X
⊢ (M ＼ e).r X = M.r X
Tactic:
rw [deleteElem, delete_r_eq', diff_singleton_eq_self heX]
State after:
no goals