apply WithTop.add_right_cancel (show (1 : ℕ∞) ≠ ⊤ from ENat.coe_toNat_eq_self.mp rfl)
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X = M.er (insert e X) - 1
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X + 1 = M.er (insert e X) - 1 + 1