[GOAL]
m n : ℕ
hne : m ≠ n
⊢ ↑m ≠ ↑n
[PROOFSTEP]
exact_mod_cast hne
[GOAL]
x : ℕ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
[PROOFSTEP]
rcases le_or_lt 0 r with (hr | hr)
[GOAL]
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
[PROOFSTEP]
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
[GOAL]
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ ↑x + r
[PROOFSTEP]
exact add_nonneg (cast_nonneg x) hr
[GOAL]
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
[PROOFSTEP]
rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]
[GOAL]
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x + r⌋₊ < ⌈↑x - r⌉₊
[PROOFSTEP]
calc
  ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
  _ < ⌈↑x - r⌉₊ := by
    rw [floor_coe, Nat.lt_ceil]
    linarith
[GOAL]
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x + r ≤ ↑x
[PROOFSTEP]
linarith
[GOAL]
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x⌋₊ < ⌈↑x - r⌉₊
[PROOFSTEP]
rw [floor_coe, Nat.lt_ceil]
[GOAL]
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x < ↑x - r
[PROOFSTEP]
linarith
[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]
⊢ NeBot (cocompact ℕ)
[PROOFSTEP]
simp [Filter.atTop_neBot]
