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

State before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hDX : Disjoint X D
⊢ (M ＼ D).r X = M.r X
Tactic:
rw [delete_r_eq', hDX.sdiff_eq_left]
State after:
no goals