case h
p x ε y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ closedBall x ε
p x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = closedBall x ε
ext y
no goals
case h
p x ε y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ closedBall x ε
simp only [Set.mem_preimage, dist_eq_norm, AddCircle.norm_eq_of_zero, iff_self,
  ← QuotientAddGroup.mk_sub, Metric.mem_closedBall, Real.norm_eq_abs]