exact (M.er_contract_le_er _ _).trans (M.er_mono diff_subset)
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
I J C✝ D✝ X Y Z : Set α
e f : α
C D : Set α
⊢ (M ／ C).er (univ \ D) ≤ M.er univ
no goals