no goals
F : Type u_3
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedRing β
inst✝² : FloorRing α
inst✝¹ : FloorRing β
inst✝ : RingHomClass F α β
a✝ : α
b : β
f : F
hf : StrictMono ↑f
a : α
n : ℤ
⊢ ↑f a ≤ ↑n ↔ a ≤ ↑n
rw [← map_intCast f, hf.le_iff_le]