simp_rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add, coe_r_eq, ← relRank_add_er_eq, relRank]
α : 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 C = M.r (X ∪ C)
no goals