Theorem: Matroid.Nonloop.contract_r_cast_int_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 α
inst✝ : M.FiniteRk
he : M.Nonloop e
⊢ ↑((M ／ e).r X) = ↑(M.r (insert e X)) - 1
Tactic:
rw [← he.contract_r_add_one_eq]
State after:
α : 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

State before:
α : 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
Tactic:
exact eq_sub_of_add_eq rfl
State after:
no goals