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