English
Two angles are equal if and only if they have the same sign and equal absolute values of their real representations.
Русский
Два угла равны тогда и только тогда, когда у них одинаковый знак и равны модули их действительных представлений.
LaTeX
$$θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|$$
Lean4
theorem eq_iff_sign_eq_and_abs_toReal_eq {θ ψ : Angle} : θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal| :=
by
refine ⟨?_, fun h => ?_⟩
· rintro rfl
exact ⟨rfl, rfl⟩
rcases h with ⟨hs, hr⟩
rw [abs_eq_abs] at hr
rcases hr with (hr | hr)
· exact toReal_injective hr
· by_cases h : θ = π
· rw [h, toReal_pi, ← neg_eq_iff_eq_neg] at hr
exact False.elim ((neg_pi_lt_toReal ψ).ne hr)
· by_cases h' : ψ = π
· rw [h', toReal_pi] at hr
exact False.elim ((neg_pi_lt_toReal θ).ne hr.symm)
· rw [← sign_toReal h, ← sign_toReal h', hr, Left.sign_neg, SignType.neg_eq_self_iff, _root_.sign_eq_zero_iff,
toReal_eq_zero_iff] at hs
rw [hs, toReal_zero, neg_zero, toReal_eq_zero_iff] at hr
rw [hr, hs]
