rw [relRank, ← er_inter_ground_eq, ← hI.encard, ← hI.indep.of_contract.er]
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y I : Set α
hI : (M ／ X).Basis I (Y ∩ (M ／ X).E)
⊢ M.relRank X Y ≤ M.er Y
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y I : Set α
hI : (M ／ X).Basis I (Y ∩ (M ／ X).E)
⊢ M.er I ≤ M.er Y