-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem eq_iff_sign_eq_and_abs_toReal_eq {θ ψ : Angle} :
    θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|

Proof state:
case refine_2.intro
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : |θ.toReal| = |ψ.toReal|
⊢ θ = ψ

Tactic:
rw [abs_eq_abs] at hr

Result:
case refine_2.intro
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = ψ.toReal ∨ θ.toReal = -ψ.toReal
⊢ θ = ψ

Proof state:
case pos
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -π
h : ¬θ = ↑π
h' : ψ = ↑π
⊢ θ = ψ

Tactic:
exact False.elim ((neg_pi_lt_toReal θ).ne hr.symm)

Result:
no goals

Proof state:
θ ψ : Angle
⊢ θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|

Tactic:
refine ⟨?_, fun h => ?_⟩

Result:
case refine_1
θ ψ : Angle
⊢ θ = ψ → θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|

case refine_2
θ ψ : Angle
h : θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|
⊢ θ = ψ

Proof state:
case pos
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : -π = ψ.toReal
h : θ = ↑π
⊢ θ = ψ

Tactic:
exact False.elim ((neg_pi_lt_toReal ψ).ne hr)

Result:
no goals

Proof state:
case neg
θ ψ : Angle
hs : ψ = 0
hr : θ = 0
h : ¬θ = ↑π
h' : ¬ψ = ↑π
⊢ θ = ψ

Tactic:
rw [hr, hs]

Result:
no goals

Proof state:
case neg
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
h : ¬θ = ↑π
h' : ¬ψ = ↑π
⊢ θ = ψ

Tactic:
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

Result:
case neg
θ ψ : Angle
hs : ψ = 0
hr : θ.toReal = -ψ.toReal
h : ¬θ = ↑π
h' : ¬ψ = ↑π
⊢ θ = ψ

Proof state:
case refine_2
θ ψ : Angle
h : θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|
⊢ θ = ψ

Tactic:
rcases h with ⟨hs, hr⟩

Result:
case refine_2.intro
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : |θ.toReal| = |ψ.toReal|
⊢ θ = ψ

Proof state:
case refine_2.intro
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = ψ.toReal ∨ θ.toReal = -ψ.toReal
⊢ θ = ψ

Tactic:
rcases hr with (hr | hr)

Result:
case refine_2.intro.inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = ψ.toReal
⊢ θ = ψ

case refine_2.intro.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
⊢ θ = ψ

Proof state:
case pos
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
h : ¬θ = ↑π
h' : ψ = ↑π
⊢ θ = ψ

Tactic:
rw [h', toReal_pi] at hr

Result:
case pos
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -π
h : ¬θ = ↑π
h' : ψ = ↑π
⊢ θ = ψ

Proof state:
case refine_1
θ : Angle
⊢ θ.sign = θ.sign ∧ |θ.toReal| = |θ.toReal|

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
case refine_1
θ ψ : Angle
⊢ θ = ψ → θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|

Tactic:
rintro rfl

Result:
case refine_1
θ : Angle
⊢ θ.sign = θ.sign ∧ |θ.toReal| = |θ.toReal|

Proof state:
case neg
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
h : ¬θ = ↑π
⊢ θ = ψ

Tactic:
by_cases h' : ψ = π

Result:
case pos
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
h : ¬θ = ↑π
h' : ψ = ↑π
⊢ θ = ψ

case neg
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
h : ¬θ = ↑π
h' : ¬ψ = ↑π
⊢ θ = ψ

Proof state:
case neg
θ ψ : Angle
hs : ψ = 0
hr : θ.toReal = -ψ.toReal
h : ¬θ = ↑π
h' : ¬ψ = ↑π
⊢ θ = ψ

Tactic:
rw [hs, toReal_zero, neg_zero, toReal_eq_zero_iff] at hr

Result:
case neg
θ ψ : Angle
hs : ψ = 0
hr : θ = 0
h : ¬θ = ↑π
h' : ¬ψ = ↑π
⊢ θ = ψ

Proof state:
case refine_2.intro.inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = ψ.toReal
⊢ θ = ψ

Tactic:
exact toReal_injective hr

Result:
no goals

Proof state:
case refine_2.intro.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
⊢ θ = ψ

Tactic:
by_cases h : θ = π

Result:
case pos
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
h : θ = ↑π
⊢ θ = ψ

case neg
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
h : ¬θ = ↑π
⊢ θ = ψ

Proof state:
case pos
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : θ.toReal = -ψ.toReal
h : θ = ↑π
⊢ θ = ψ

Tactic:
rw [h, toReal_pi, ← neg_eq_iff_eq_neg] at hr

Result:
case pos
θ ψ : Angle
hs : θ.sign = ψ.sign
hr : -π = ψ.toReal
h : θ = ↑π
⊢ θ = ψ