case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
x : ℕ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
rcases le_or_lt 0 r with (hr | hr)
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ ↑x + r
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
no goals
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ ↑x + r
exact add_nonneg (cast_nonneg x) hr
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x + r⌋₊ < ⌈↑x - r⌉₊
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]
no goals
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x + r⌋₊ < ⌈↑x - r⌉₊
calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
_ < ⌈↑x - r⌉₊ := by
  rw [floor_coe, Nat.lt_ceil]
  linarith
no goals
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x + r ≤ ↑x
linarith
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x < ↑x - r
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x⌋₊ < ⌈↑x - r⌉₊
rw [floor_coe, Nat.lt_ceil]
no goals
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x < ↑x - r
linarith