English
For real numbers θ and ψ, cos θ = cos ψ holds exactly when the angle corresponding to θ equals ψ or equals −ψ.
Русский
Пусть θ и ψ — действительные числа. Тогда cos θ = cos ψ эквивалентно тому, что угол, соответствующий θ, равен ψ или равен −ψ.
LaTeX
$$$\cos \theta = \cos \psi \iff \theta = \psi \;\lor\; \theta = -\psi$$$
Lean4
theorem cos_eq_iff_coe_eq_or_eq_neg {θ ψ : ℝ} : cos θ = cos ψ ↔ (θ : Angle) = ψ ∨ (θ : Angle) = -ψ :=
by
constructor
· intro Hcos
rw [← sub_eq_zero, cos_sub_cos, mul_eq_zero, mul_eq_zero, neg_eq_zero, eq_false (two_ne_zero' ℝ), false_or,
sin_eq_zero_iff, sin_eq_zero_iff] at Hcos
rcases Hcos with (⟨n, hn⟩ | ⟨n, hn⟩)
· right
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), ← sub_eq_iff_eq_add] at hn
rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi,
zsmul_zero]
· left
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), eq_sub_iff_add_eq] at hn
rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero, zero_add]
· rw [angle_eq_iff_two_pi_dvd_sub, ← coe_neg, angle_eq_iff_two_pi_dvd_sub]
rintro (⟨k, H⟩ | ⟨k, H⟩)
·
rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _,
sin_int_mul_pi, mul_zero]
rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
