p x : ℝ
⊢ {y | ↑y = ↑x} = {x}
p x : ℝ
⊢ ‖↑x‖ = abs x
suffices { y : ℝ | (y : AddCircle (0 : ℝ)) = (x : AddCircle (0 : ℝ)) } = {x} by
  rw [quotient_norm_eq, this, image_singleton, Real.norm_eq_abs, csInf_singleton]
case h
p x y : ℝ
⊢ y ∈ {y | ↑y = ↑x} ↔ y ∈ {x}
p x : ℝ
⊢ {y | ↑y = ↑x} = {x}
ext y
no goals
case h
p x y : ℝ
⊢ y ∈ {y | ↑y = ↑x} ↔ y ∈ {x}
simp [QuotientAddGroup.eq_iff_sub_mem, mem_zmultiples_iff, sub_eq_zero]
no goals
p x : ℝ
this : {y | ↑y = ↑x} = {x}
⊢ ‖↑x‖ = abs x
rw [quotient_norm_eq, this, image_singleton, Real.norm_eq_abs, csInf_singleton]