English
For real numbers θ and ψ, sin θ = sin ψ iff the angle corresponding to θ equals ψ or θ + ψ = π.
Русский
Пусть θ, ψ — действительные числа. Тогда sin θ = sin ψ эквивалентно тому, что угол θ равен ψ или что θ + ψ = π.
LaTeX
$$$\sin \theta = \sin \psi \iff \theta = \psi \;\lor\; \theta + \psi = \pi$$$
Lean4
theorem sin_eq_iff_coe_eq_or_add_eq_pi {θ ψ : ℝ} : sin θ = sin ψ ↔ (θ : Angle) = ψ ∨ (θ : Angle) + ψ = π :=
by
constructor
· intro Hsin
rw [← cos_pi_div_two_sub, ← cos_pi_div_two_sub] at Hsin
rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hsin with h | h
· left
rw [coe_sub, coe_sub] at h
exact sub_right_inj.1 h
right
rw [coe_sub, coe_sub, eq_neg_iff_add_eq_zero, add_sub, sub_add_eq_add_sub, ← coe_add, add_halves, sub_sub,
sub_eq_zero] at h
exact h.symm
· rw [angle_eq_iff_two_pi_dvd_sub, ← eq_sub_iff_add_eq, ← coe_sub, angle_eq_iff_two_pi_dvd_sub]
rintro (⟨k, H⟩ | ⟨k, H⟩)
·
rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _,
sin_int_mul_pi, mul_zero, zero_mul]
have H' : θ + ψ = 2 * k * π + π := by
rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ← mul_assoc] at H
rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
cos_add_pi_div_two, sin_int_mul_pi, neg_zero, mul_zero]
