exact M.er_le_encard {e}
case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
inst✝ : M.Nonempty
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ M.E, X ⊆ M.cl {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.cl {e}
⊢ M.er {e} ≤ {e}.encard
no goals