[GOAL]
α : Type u_1
inst✝¹ : OrderedAddCommMonoid α
inst✝ : Archimedean α
x y : { x // 0 ≤ x }
hy : 0 < y
n : ℕ
hr : ↑x ≤ n • (fun a => ↑a) y
⊢ ↑x ≤ ↑(n • y)
[PROOFSTEP]
simp [*, -nsmul_eq_mul, nsmul_coe]
