q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑↑m + x)
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m + x)
rw [← cast_coe_int]
no goals
q : ℚ
x y : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑↑m + x)
exact h.rat_add m