Theorem: Matroid.Nonloop.relRank_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 : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X + 1 = M.er (insert e X)
Tactic:
rw [← union_singleton, ← relRank_add_er_eq, he.er_eq]
State after:
no goals