-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_two_nsmul_eq_sign_iff {θ : Angle} :
    ((2 : ℕ) • θ).sign = θ.sign ↔ θ = π ∨ |θ.toReal| < π / 2

Proof state:
θ : Angle
⊢ (2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2

Tactic:
by_cases hpi : θ = π

Result:
case pos
θ : Angle
hpi : θ = ↑π
⊢ (2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2

case neg
θ : Angle
hpi : ¬θ = ↑π
⊢ (2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2

Proof state:
case neg.refine_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = θ.sign
hpi' : θ.toReal ≠ π
hle : π / 2 ≤ θ.toReal
hlt : π / 2 < θ.toReal
⊢ False

Tactic:
rw [← sign_toReal hpi, sign_pos (pi_div_two_pos.trans hlt), ← sign_toReal,
  two_nsmul_toReal_eq_two_mul_sub_two_pi.2 hlt, _root_.sign_neg] at h

Result:
case neg.refine_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : -1 = 1
hpi' : θ.toReal ≠ π
hle : π / 2 ≤ θ.toReal
hlt : π / 2 < θ.toReal
⊢ False

case neg.refine_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : SignType.sign (2 * θ.toReal - 2 * π) = 1
hpi' : θ.toReal ≠ π
hle : π / 2 ≤ θ.toReal
hlt : π / 2 < θ.toReal
⊢ 2 * θ.toReal - 2 * π < 0

case neg.refine_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = 1
hpi' : θ.toReal ≠ π
hle : π / 2 ≤ θ.toReal
hlt : π / 2 < θ.toReal
⊢ 2 • θ ≠ ↑π

Proof state:
case neg.refine_1
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = θ.sign
hle : π / 2 ≤ θ.toReal ∨ θ.toReal ≤ -(π / 2)
hpi' : θ.toReal ≠ π
⊢ False

Tactic:
rcases hle with (hle | hle) <;> rcases hle.eq_or_lt with (heq | hlt)

Result:
case neg.refine_1.inl.inl
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = θ.sign
hpi' : θ.toReal ≠ π
hle : π / 2 ≤ θ.toReal
heq : π / 2 = θ.toReal
⊢ False

case neg.refine_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = θ.sign
hpi' : θ.toReal ≠ π
hle : π / 2 ≤ θ.toReal
hlt : π / 2 < θ.toReal
⊢ False

case neg.refine_1.inr.inl
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = θ.sign
hpi' : θ.toReal ≠ π
hle : θ.toReal ≤ -(π / 2)
heq : θ.toReal = -(π / 2)
⊢ False

case neg.refine_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = θ.sign
hpi' : θ.toReal ≠ π
hle : θ.toReal ≤ -(π / 2)
hlt : θ.toReal < -(π / 2)
⊢ False

Proof state:
case neg.refine_1.inr.inl
θ : Angle
hpi : ¬θ = ↑π
h : (2 • ↑(-(π / 2))).sign = (↑(-(π / 2))).sign
hpi' : θ.toReal ≠ π
hle : θ.toReal ≤ -(π / 2)
heq : θ.toReal = -(π / 2)
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
case neg.refine_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = -1
hpi' : θ.toReal ≠ π
hle : θ.toReal ≤ -(π / 2)
hlt : θ.toReal < -(π / 2)
⊢ 2 • θ ≠ ↑π

Tactic:
intro he

Result:
case neg.refine_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = -1
hpi' : θ.toReal ≠ π
hle : θ.toReal ≤ -(π / 2)
hlt : θ.toReal < -(π / 2)
he : 2 • θ = ↑π
⊢ False

Proof state:
case neg.refine_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : SignType.sign (2 • θ).toReal = -1
hpi' : θ.toReal ≠ π
hle : θ.toReal ≤ -(π / 2)
hlt : θ.toReal < -π / 2
⊢ False

Tactic:
rw [two_nsmul_toReal_eq_two_mul_add_two_pi.2 hlt.le, sign_pos] at h

Result:
case neg.refine_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : 1 = -1
hpi' : θ.toReal ≠ π
hle : θ.toReal ≤ -(π / 2)
hlt : θ.toReal < -π / 2
⊢ False

case neg.refine_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : SignType.sign (2 * θ.toReal + 2 * π) = -1
hpi' : θ.toReal ≠ π
hle : θ.toReal ≤ -(π / 2)
hlt : θ.toReal < -π / 2
⊢ 0 < 2 * θ.toReal + 2 * π

Proof state:
case neg.refine_2
θ : Angle
hpi : ¬θ = ↑π
h : |θ.toReal| < π / 2
hpi' : 2 • θ ≠ ↑π
⊢ (2 • θ).sign = θ.sign

Tactic:
rw [abs_lt, ← neg_div] at h

Result:
case neg.refine_2
θ : Angle
hpi : ¬θ = ↑π
h : -π / 2 < θ.toReal ∧ θ.toReal < π / 2
hpi' : 2 • θ ≠ ↑π
⊢ (2 • θ).sign = θ.sign

Proof state:
case pos
θ : Angle
hpi : θ = ↑π
⊢ (2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2

Tactic:
simp [hpi]

Result:
no goals

Proof state:
case neg.refine_1
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = θ.sign
hle : π / 2 ≤ θ.toReal ∨ θ.toReal ≤ -(π / 2)
⊢ False

Tactic:
have hpi' : θ.toReal ≠ π := by simpa using hpi

Result:
case neg.refine_1
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = θ.sign
hle : π / 2 ≤ θ.toReal ∨ θ.toReal ≤ -(π / 2)
hpi' : θ.toReal ≠ π
⊢ False