Unecessarily complex goal

Stream: mathlib4

[Eric Wieser]

Guess what the goal is at this sorry?

import Mathlib

example (z : ℤ) : |(z : ℝ)| ≤ z := by
  simp
  sorry

Complex.abs ↑z ≤ ↑z, due to docs#Complex.int_cast_abs / docs3#complex.int_cast_abs