Theorem: Matroid.Nonloop.contract_r_add_one_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 + 1 = M.r (insert e X)
Tactic:
rw [← union_singleton, ← contract_r_add_eq, he.r_eq, contract_elem]
State after:
no goals