rw [relRank, relRank, ← union_diff_cancel h, ← contract_contract]
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X X' Y : Set α
h : X ⊆ X'
⊢ M.relRank X' Y ≤ M.relRank X Y
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X X' Y : Set α
h : X ⊆ X'
⊢ (M ／ X ／ (X' \ X)).er Y ≤ (M ／ X).er Y