F : Type u_3
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : LinearOrderedField β
inst✝² : FloorRing α
inst✝¹ : FloorRing β
inst✝ : RingHomClass F α β
a✝ : α
b : β
f : F
hf : StrictMono ↑f
a : α
H : ↑f 2 = 2
⊢ round (↑f a) = round a
F : Type u_3
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : LinearOrderedField β
inst✝² : FloorRing α
inst✝¹ : FloorRing β
inst✝ : RingHomClass F α β
a✝ : α
b : β
f : F
hf : StrictMono ↑f
a : α
⊢ round (↑f a) = round a
have H : f 2 = 2 := map_natCast f 2
no goals
F : Type u_3
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : LinearOrderedField β
inst✝² : FloorRing α
inst✝¹ : FloorRing β
inst✝ : RingHomClass F α β
a✝ : α
b : β
f : F
hf : StrictMono ↑f
a : α
H : ↑f 2 = 2
⊢ round (↑f a) = round a
simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, H]