[GOAL]
⊢ AbsoluteValue.uniformSpace AbsoluteValue.abs = PseudoMetricSpace.toUniformSpace
[PROOFSTEP]
ext s
[GOAL]
case a.a
s : Set (ℚ × ℚ)
⊢ s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ
[PROOFSTEP]
rw [(AbsoluteValue.hasBasis_uniformity _).mem_iff, Metric.uniformity_basis_dist_rat.mem_iff]
[GOAL]
case a.a
s : Set (ℚ × ℚ)
⊢ (∃ i, 0 < i ∧ {p | ↑AbsoluteValue.abs (p.snd - p.fst) < i} ⊆ s) ↔ ∃ i, 0 < i ∧ {p | dist p.fst p.snd < ↑i} ⊆ s
[PROOFSTEP]
simp only [Rat.dist_eq, AbsoluteValue.abs_apply, ← Rat.cast_sub, ← Rat.cast_abs, Rat.cast_lt, abs_sub_comm]
[GOAL]
⊢ UniformSpace ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CompleteSpace ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ SeparatedSpace ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ UniformInducing Rat.cast
[PROOFSTEP]
rw [Rat.uniformSpace_eq]
[GOAL]
⊢ UniformInducing Rat.cast
[PROOFSTEP]
exact Rat.uniformEmbedding_coe_real.toUniformInducing
