apply WithTop.add_right_cancel <| ne_top_of_lt hY
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y = M.relRank X Y + M.er X - M.er X
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y + M.er X = M.relRank X Y + M.er X - M.er X + M.er X