rw [relRank_eq_er_diff_contract,  relRank, ← (M ／ X).er_cl_eq Y, contract_cl_eq]
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X (M.cl Y) ≤ M.relRank X Y
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er (M.cl Y \ X) ≤ (M ／ X).er (M.cl (Y ∪ X) \ X)