English
If cos θ = cos ψ and sin θ = sin ψ for real numbers θ, ψ, then θ = ψ.
Русский
Если cos θ = cos ψ и sin θ = sin ψ для действительных θ, ψ, тогда следует θ = ψ.
LaTeX
$$(\cos \theta = \cos \psi) \land (\sin \theta = \sin \psi) \Rightarrow \theta = \psi$$
Lean4
theorem cos_sin_inj {θ ψ : ℝ} (Hcos : cos θ = cos ψ) (Hsin : sin θ = sin ψ) : (θ : Angle) = ψ :=
by
rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hcos with hc | hc; · exact hc
rcases sin_eq_iff_coe_eq_or_add_eq_pi.mp Hsin with hs | hs; · exact hs
rw [eq_neg_iff_add_eq_zero, hs] at hc
obtain ⟨n, hn⟩ : ∃ n, n • _ = _ := QuotientAddGroup.leftRel_apply.mp (Quotient.exact' hc)
rw [← neg_one_mul, add_zero, ← sub_eq_zero, zsmul_eq_mul, ← mul_assoc, ← sub_mul, mul_eq_zero,
eq_false (ne_of_gt pi_pos), or_false, sub_neg_eq_add, ← Int.cast_zero, ← Int.cast_one, ← Int.cast_ofNat, ←
Int.cast_mul, ← Int.cast_add, Int.cast_inj] at hn
have : (n * 2 + 1) % (2 : ℤ) = 0 % (2 : ℤ) := congr_arg (· % (2 : ℤ)) hn
rw [add_comm, Int.add_mul_emod_self_right] at this
exact absurd this one_ne_zero
