English
For complex x and y, cos x = cos y if and only if there exists an integer k such that y = 2kπ ± x.
Русский
Для комплексных x, y: cos x = cos y тогда и только тогда, когда существует целое k такое, что y = 2kπ ± x.
LaTeX
$$$$\\cos x = \\cos y \\iff \\exists k \\in \\mathbb{Z}, y = 2 k \\pi \\pm x$$$$
Lean4
theorem cos_eq_cos_iff {x y : ℂ} : cos x = cos y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x :=
calc
cos x = cos y ↔ cos x - cos y = 0 := sub_eq_zero.symm
_ ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0 := by rw [cos_sub_cos]
_ ↔ sin ((x + y) / 2) = 0 ∨ sin ((x - y) / 2) = 0 := by simp [(by simp : (2 : ℂ) ≠ 0)]
_ ↔ sin ((x - y) / 2) = 0 ∨ sin ((x + y) / 2) = 0 := or_comm
_ ↔ (∃ k : ℤ, y = 2 * k * π + x) ∨ ∃ k : ℤ, y = 2 * k * π - x :=
by
apply or_congr <;>
simp [field, sin_eq_zero_iff, eq_sub_iff_add_eq', sub_eq_iff_eq_add, mul_comm (2 : ℂ), mul_right_comm _ (2 : ℂ)]
constructor <;> · rintro ⟨k, rfl⟩; use -k; simp
_ ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x := exists_or.symm
