obtain ⟨C, D, -, -, -, rfl⟩ := h
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
⊢ N.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 ＼ D).erk ≤ M.erk