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

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

Tactic:
simp [he] at h

Result:
no goals

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

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

Tactic:
swap

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

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

Proof state:
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 - π) < 0

Tactic:
exact mul_neg_of_pos_of_neg two_pos (sub_neg.2 ((toReal_le_pi _).lt_of_ne hpi'))

Result:
no goals

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

Tactic:
simp [he] at h

Result:
no goals

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

Tactic:
rw [← coe_toReal θ, heq] at h

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

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

Tactic:
rw [← sign_toReal hpi, ← sign_toReal hpi', two_nsmul_toReal_eq_two_mul.2 ⟨h.1, h.2.le⟩,
  sign_mul, sign_pos (zero_lt_two' ℝ), one_mul]

Result:
no goals

Proof state:
case left
θ : Angle
hpi : ¬θ = ↑π
h : |θ.toReal| < π / 2
⊢ ¬θ = ↑(π / 2)

Tactic:
rintro rfl

Result:
case left
hpi : ¬↑(π / 2) = ↑π
h : |(↑(π / 2)).toReal| < π / 2
⊢ False

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

Tactic:
rw [or_iff_right hpi]

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

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 [← neg_div] at hlt

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

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

Tactic:
simpa using hpi

Result:
no goals

Proof state:
case right
θ : Angle
hpi : ¬θ = ↑π
h : |θ.toReal| < π / 2
⊢ ¬θ = ↑(-π / 2)

Tactic:
rintro rfl

Result:
case right
hpi : ¬↑(-π / 2) = ↑π
h : |(↑(-π / 2)).toReal| < π / 2
⊢ False

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

Tactic:
intro he

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

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

Tactic:
simp at h

Result:
no goals

Proof state:
case left
hpi : ¬↑(π / 2) = ↑π
h : |(↑(π / 2)).toReal| < π / 2
⊢ False

Tactic:
simp [pi_pos, div_pos, abs_of_pos] at h

Result:
no goals

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

Tactic:
simp at h

Result:
no goals

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

Tactic:
simp at h

Result:
no goals

Proof state:
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 * π

Tactic:
linarith [neg_pi_lt_toReal θ]

Result:
no goals

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

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

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

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

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

Tactic:
by_contra hle

Result:
case neg.refine_1
θ : Angle
hpi : ¬θ = ↑π
h : (2 • θ).sign = θ.sign
hle : ¬|θ.toReal| < π / 2
⊢ False

Proof state:
θ : Angle
hpi : ¬θ = ↑π
h : |θ.toReal| < π / 2
⊢ ¬θ = ↑(π / 2) ∧ ¬θ = ↑(-π / 2)

Tactic:
constructor

Result:
case left
θ : Angle
hpi : ¬θ = ↑π
h : |θ.toReal| < π / 2
⊢ ¬θ = ↑(π / 2)

case right
θ : Angle
hpi : ¬θ = ↑π
h : |θ.toReal| < π / 2
⊢ ¬θ = ↑(-π / 2)

Proof state:
case right
hpi : ¬↑(-π / 2) = ↑π
h : |-π / 2| < π / 2
⊢ False

Tactic:
simp [pi_pos, div_pos, neg_div, abs_of_pos] at h

Result:
no goals

Proof state:
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

Tactic:
rw [← mul_sub]

Result:
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 - π) < 0

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

Tactic:
rw [not_lt, le_abs, le_neg] at hle

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

Proof state:
θ : Angle
hpi : ¬θ = ↑π
h : |θ.toReal| < π / 2
⊢ 2 • θ ≠ ↑π

Tactic:
rw [Ne, two_nsmul_eq_pi_iff, not_or]

Result:
θ : Angle
hpi : ¬θ = ↑π
h : |θ.toReal| < π / 2
⊢ ¬θ = ↑(π / 2) ∧ ¬θ = ↑(-π / 2)

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

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

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

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

Proof state:
case right
hpi : ¬↑(-π / 2) = ↑π
h : |(↑(-π / 2)).toReal| < π / 2
⊢ False

Tactic:
rw [toReal_neg_pi_div_two] at h

Result:
case right
hpi : ¬↑(-π / 2) = ↑π
h : |-π / 2| < π / 2
⊢ False

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

Tactic:
rw [← coe_toReal θ, ← heq] at h

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