α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
⊢ round ↑x = round x
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ round ↑x = round x
have H : ((2 : ℚ) : α) = (2 : α) := Rat.cast_coe_nat 2
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ round ↑x = round x
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
⊢ round ↑x = round x
have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp [H]
no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ round ↑x = round x
rw [round_eq, round_eq, ← this, floor_cast]
no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
⊢ ↑(x + 1 / 2) = ↑x + 1 / 2
simp [H]