rw [← er_univ_eq, ← er_univ_eq, delete_er_eq']
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 ＼ D).erk ≤ M.erk
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