Theorem: Matroid.relRank_add_er_of_subset (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
⊢ M.relRank X Y + M.er X = M.er Y
Tactic:
rw [relRank_add_er_eq, union_eq_self_of_subset_right hXY]
State after:
no goals