refine (M.er_mono hXY).eq_of_not_lt (fun hlt ↦ ?_)
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
⊢ M.er X = M.er Y
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
hlt : M.er X < M.er Y
⊢ False