rw [← M.coe_rk_eq, ← N.coe_rk_eq] at hle
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : N.erk ≤ M.erk
this : N.FiniteRk
⊢ N.rk ≤ M.rk
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : ↑N.rk ≤ ↑M.rk
this : N.FiniteRk
⊢ N.rk ≤ M.rk