obtain ⟨I, hI⟩ := (M ／ C).exists_basis (X ∩ (M ／ C).E)
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X : Set α
⊢ (M ／ C).er X ≤ M.er X
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X I : Set α
hI : (M ／ C).Basis I (X ∩ (M ／ C).E)
⊢ (M ／ C).er X ≤ M.er X