case inl
x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ (z : ℤ), closedBall (x + z • 0) ε

case inr
p x ε : ℝ
hp : p ≠ 0
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ (z : ℤ), closedBall (x + z • p) ε
p x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ (z : ℤ), closedBall (x + z • p) ε
rcases eq_or_ne p 0 with (rfl | hp)
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ ⋃ (z : ℤ), closedBall (x + z • p) ε
case inr
p x ε : ℝ
hp : p ≠ 0
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ (z : ℤ), closedBall (x + z • p) ε
ext y
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ abs (y - x - ↑(round (p⁻¹ * (y - x))) * p) ≤ ε ↔ ∃ i, abs (y - x - ↑i * p) ≤ ε
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ ⋃ (z : ℤ), closedBall (x + z • p) ε
simp only [dist_eq_norm, mem_preimage, mem_closedBall, zsmul_eq_mul, mem_iUnion, Real.norm_eq_abs,
  ← QuotientAddGroup.mk_sub, norm_eq, ← sub_sub]
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ (∃ i, abs (y - x - ↑i * p) ≤ ε) → abs (y - x - ↑(round (p⁻¹ * (y - x))) * p) ≤ ε
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ abs (y - x - ↑(round (p⁻¹ * (y - x))) * p) ≤ ε ↔ ∃ i, abs (y - x - ↑i * p) ≤ ε
refine' ⟨fun h => ⟨round (p⁻¹ * (y - x)), h⟩, _⟩
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : abs (y - x - ↑n * p) ≤ ε
⊢ abs (y - x - ↑(round (p⁻¹ * (y - x))) * p) ≤ ε
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ (∃ i, abs (y - x - ↑i * p) ≤ ε) → abs (y - x - ↑(round (p⁻¹ * (y - x))) * p) ≤ ε
rintro ⟨n, hn⟩
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : abs (p⁻¹ * (y - x) - ↑n) ≤ abs p⁻¹ * ε
⊢ abs (p⁻¹ * (y - x) - ↑(round (p⁻¹ * (y - x)))) ≤ abs p⁻¹ * ε
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : abs (y - x - ↑n * p) ≤ ε
⊢ abs (y - x - ↑(round (p⁻¹ * (y - x))) * p) ≤ ε
rw [← mul_le_mul_left (abs_pos.mpr <| inv_ne_zero hp), ← abs_mul, mul_sub, mul_comm _ p,
  inv_mul_cancel_left₀ hp] at hn⊢
no goals
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : abs (p⁻¹ * (y - x) - ↑n) ≤ abs p⁻¹ * ε
⊢ abs (p⁻¹ * (y - x) - ↑(round (p⁻¹ * (y - x)))) ≤ abs p⁻¹ * ε
exact (round_le (p⁻¹ * (y - x)) n).trans hn
no goals
case inl
x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ (z : ℤ), closedBall (x + z • 0) ε
simp [iUnion_const]