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