rw [relRank, ← er_inter_ground_eq, contract_ground, ← inter_diff_assoc]
case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X Y ≤ M.relRank X (M.cl Y)
case refine_2
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er ((Y ∩ M.E) \ X) ≤ M.relRank X (M.cl Y)