rw [← union_singleton, ← contract_r_add_eq, he.r_eq, contract_elem]
α : 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)
no goals