Theorem: Matroid.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
C X : Set α
⊢ ↑((M ／ C).r X) = ↑(M.r (X ∪ C)) - ↑(M.r C)
Tactic:
rw [← contract_r_add_eq]
State after:
α : 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)

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