[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]


[GOAL]
x y : ℕ
⊢ dist ↑x ↑y = dist x y
[PROOFSTEP]
rw [← Nat.dist_cast_real, ← Rat.dist_cast]
[GOAL]
x y : ℕ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y
[PROOFSTEP]
congr
[GOAL]
⊢ Pairwise fun x y => 1 ≤ dist ↑x ↑y
[PROOFSTEP]
simpa using Nat.pairwise_one_le_dist
[GOAL]
⊢ Pairwise fun x y => 1 ≤ dist ↑x ↑y
[PROOFSTEP]
simpa using Nat.pairwise_one_le_dist
[GOAL]
x y : ℤ
⊢ dist ↑x ↑y = dist x y
[PROOFSTEP]
rw [← Int.dist_cast_real, ← Rat.dist_cast]
[GOAL]
x y : ℤ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y
[PROOFSTEP]
congr
[GOAL]
⊢ Pairwise fun x y => 1 ≤ dist ↑x ↑y
[PROOFSTEP]
simpa using Int.pairwise_one_le_dist
[GOAL]
⊢ Pairwise fun x y => 1 ≤ dist ↑x ↑y
[PROOFSTEP]
simpa using Int.pairwise_one_le_dist
[GOAL]
⊢ UniformContinuous (Rat.cast ∘ fun p => p.fst + p.snd)
[PROOFSTEP]
simp only [(· ∘ ·), Rat.cast_add]
[GOAL]
⊢ UniformContinuous fun x => ↑x.fst + ↑x.snd
[PROOFSTEP]
exact Real.uniformContinuous_add.comp (Rat.uniformContinuous_coe_real.prod_map Rat.uniformContinuous_coe_real)
[GOAL]
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℚ
h : dist a✝ b✝ < ε
⊢ dist (-a✝) (-b✝) < ε
[PROOFSTEP]
rw [dist_comm] at h
[GOAL]
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℚ
h : dist b✝ a✝ < ε
⊢ dist (-a✝) (-b✝) < ε
[PROOFSTEP]
simpa only [dist_eq, cast_neg, neg_sub_neg] using h
[GOAL]
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℚ
h : dist a✝ b✝ < ε
⊢ dist |a✝| |b✝| ≤ dist a✝ b✝
[PROOFSTEP]
simpa [Rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _
[GOAL]
a b : ℚ
⊢ TotallyBounded (Icc a b)
[PROOFSTEP]
simpa only [preimage_cast_Icc] using
  totallyBounded_preimage Rat.uniformEmbedding_coe_real (totallyBounded_Icc (a : ℝ) b)


[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h : x ≠ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
obtain h | h := h.not_le_or_not_le
[GOAL]
case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬x ≤ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
exact (exists_clopen_upper_of_not_le h).imp fun _ ↦ And.imp_right <| And.imp_left Or.inl
[GOAL]
case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
obtain ⟨U, hU, hU', hy, hx⟩ := exists_clopen_lower_of_not_le h
[GOAL]
case inr.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
U : Set α
hU : IsClopen U
hU' : IsLowerSet U
hy : ¬y ∈ U
hx : x ∈ U
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
exact ⟨U, hU, Or.inr hU', hx, hy⟩