exact er_mono _ <| diff_subset.trans
  ((M.subset_cl _).trans (M.cl_subset_cl inter_subset_left))
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)
no goals