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