exact (M ／ X).er_mono (diff_subset_diff_left (M.cl_subset_cl subset_union_left))
case refine_1
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ (M ／ X).er (M.cl Y \ X) ≤ (M ／ X).er (M.cl (Y ∪ X) \ X)
no goals