⊢ comap (fun y => ↑(abs y)) atTop = comap (Int.cast ∘ abs) atTop
⊢ cocompact ℤ = atBot ⊔ atTop
simp_rw [← comap_dist_right_atTop_eq_cocompact (0 : ℤ), dist_eq', sub_zero,
  ← comap_abs_atTop, ← @Int.comap_cast_atTop ℝ, comap_comap]
no goals
⊢ comap (fun y => ↑(abs y)) atTop = comap (Int.cast ∘ abs) atTop
rfl