rw [← he.relRank_add_one_eq, eq_comm, tsub_add_cancel_iff_le]
α : 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
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ 1 ≤ M.relRank {e} X + 1