[GOAL]
m n : ℤ
⊢ dist m n = ↑|m - n|
[PROOFSTEP]
rw [dist_eq]
[GOAL]
m n : ℤ
⊢ |↑m - ↑n| = ↑|m - n|
[PROOFSTEP]
norm_cast
[GOAL]
⊢ Pairwise fun m n => 1 ≤ dist m n
[PROOFSTEP]
intro m n hne
[GOAL]
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n
[PROOFSTEP]
rw [dist_eq]
[GOAL]
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |↑m - ↑n|
[PROOFSTEP]
norm_cast
[GOAL]
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |m - n|
[PROOFSTEP]
rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
[GOAL]
x : ℤ
r : ℝ
⊢ ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉
[PROOFSTEP]
rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]
[GOAL]
x : ℤ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋
[PROOFSTEP]
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
[GOAL]
x : ℤ
r : ℝ
⊢ IsCompact (closedBall x r)
[PROOFSTEP]
rw [closedBall_eq_Icc]
[GOAL]
x : ℤ
r : ℝ
⊢ IsCompact (Icc ⌈↑x - r⌉ ⌊↑x + r⌋)
[PROOFSTEP]
exact (Set.finite_Icc _ _).isCompact
[GOAL]
⊢ cocompact ℤ = atBot ⊔ atTop
[PROOFSTEP]
simp_rw [← comap_dist_right_atTop_eq_cocompact (0 : ℤ), dist_eq', sub_zero, ← comap_abs_atTop, ←
  @Int.comap_cast_atTop ℝ, comap_comap]
[GOAL]
⊢ comap (fun y => ↑|y|) atTop = comap (Int.cast ∘ abs) atTop
[PROOFSTEP]
rfl
[GOAL]
⊢ cofinite = atBot ⊔ atTop
[PROOFSTEP]
rw [← cocompact_eq_cofinite, cocompact_eq]
