English
If R ≠ 0, |a - b| < 2π, and circleMap c R a = circleMap c R b, then a = b.
Русский
Если R ≠ 0, |a - b| < 2π и circleMap c R a = circleMap c R b, то a = b.
LaTeX
$$$ R \neq 0 \land |a - b| < 2 \pi \land circleMap c R a = circleMap c R b \Rightarrow a = b $$$
Lean4
theorem eq_of_circleMap_eq {a b R : ℝ} {c : ℂ} (h_R : R ≠ 0) (h_dist : |a - b| < 2 * π)
(h : circleMap c R a = circleMap c R b) : a = b :=
by
rw [circleMap_eq_circleMap_iff c h_R] at h
obtain ⟨n, hn⟩ := h
simp only [show n * (2 * π * I) = (n * 2 * π) * I by ring, ← add_mul, mul_eq_mul_right_iff, I_ne_zero, or_false] at hn
norm_cast at hn
simp only [hn, Int.cast_mul, Int.cast_ofNat, mul_assoc, add_sub_cancel_left, abs_mul, Nat.abs_ofNat,
abs_of_pos Real.pi_pos] at h_dist
simp (disch := positivity) at h_dist
norm_cast at h_dist
simp [hn, Int.abs_lt_one_iff.mp h_dist]
