rw [← contract_r_add_eq]
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
C X : Set α
⊢ ↑((M ／ C).r X) = ↑(M.r (X ∪ C)) - ↑(M.r C)
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
C X : Set α
⊢ ↑((M ／ C).r X) = ↑((M ／ C).r X + M.r C) - ↑(M.r C)