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

case neg
θ : Angle
hpi : ¬θ = ↑π
⊢ sign (2 • θ) = sign θ ↔ θ = ↑π ∨ abs (toReal θ) < π / 2
θ : Angle
⊢ sign (2 • θ) = sign θ ↔ θ = ↑π ∨ abs (toReal θ) < π / 2
by_cases hpi : θ = π
case neg
θ : Angle
hpi : ¬θ = ↑π
⊢ sign (2 • θ) = sign θ ↔ abs (toReal θ) < π / 2
case neg
θ : Angle
hpi : ¬θ = ↑π
⊢ sign (2 • θ) = sign θ ↔ θ = ↑π ∨ abs (toReal θ) < π / 2
rw [or_iff_right hpi]
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
⊢ abs (toReal θ) < π / 2

case neg.refine'_2
θ : Angle
hpi : ¬θ = ↑π
h : abs (toReal θ) < π / 2
⊢ sign (2 • θ) = sign θ
case neg
θ : Angle
hpi : ¬θ = ↑π
⊢ sign (2 • θ) = sign θ ↔ abs (toReal θ) < π / 2
refine' ⟨fun h => _, fun h => _⟩
no goals
case pos
θ : Angle
hpi : θ = ↑π
⊢ sign (2 • θ) = sign θ ↔ θ = ↑π ∨ abs (toReal θ) < π / 2
simp [hpi]
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : ¬abs (toReal θ) < π / 2
⊢ False
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
⊢ abs (toReal θ) < π / 2
by_contra hle
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : π / 2 ≤ toReal θ ∨ toReal θ ≤ -(π / 2)
⊢ False
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : ¬abs (toReal θ) < π / 2
⊢ False
rw [not_lt, le_abs, le_neg] at hle
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : π / 2 ≤ toReal θ ∨ toReal θ ≤ -(π / 2)
hpi' : toReal θ ≠ π
⊢ False
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : π / 2 ≤ toReal θ ∨ toReal θ ≤ -(π / 2)
⊢ False
have hpi' : θ.toReal ≠ π := by simpa using hpi
case neg.refine'_1.inl.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
heq : π / 2 = toReal θ
⊢ False

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

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

case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ False
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : π / 2 ≤ toReal θ ∨ toReal θ ≤ -(π / 2)
hpi' : toReal θ ≠ π
⊢ False
rcases hle with (hle | hle) <;> rcases hle.eq_or_lt with (heq | hlt)
no goals
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : π / 2 ≤ toReal θ ∨ toReal θ ≤ -(π / 2)
⊢ toReal θ ≠ π
simpa using hpi
case neg.refine'_1.inl.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • ↑(π / 2)) = sign ↑(π / 2)
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
heq : π / 2 = toReal θ
⊢ False
case neg.refine'_1.inl.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
heq : π / 2 = toReal θ
⊢ False
rw [← coe_toReal θ, ← heq] at h
no goals
case neg.refine'_1.inl.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • ↑(π / 2)) = sign ↑(π / 2)
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
heq : π / 2 = toReal θ
⊢ False
simp at h
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 : sign (2 • θ) = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
⊢ 2 • θ ≠ ↑π
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
⊢ False
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
no goals
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : -1 = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
⊢ False
simp at h
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
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
rw [← mul_sub]
no goals
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
exact mul_neg_of_pos_of_neg two_pos (sub_neg.2 ((toReal_le_pi _).lt_of_ne hpi'))
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
he : 2 • θ = ↑π
⊢ False
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
⊢ 2 • θ ≠ ↑π
intro he
no goals
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
he : 2 • θ = ↑π
⊢ False
simp [he] at h
case neg.refine'_1.inr.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • ↑(-(π / 2))) = sign ↑(-(π / 2))
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
heq : toReal θ = -(π / 2)
⊢ False
case neg.refine'_1.inr.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
heq : toReal θ = -(π / 2)
⊢ False
rw [← coe_toReal θ, heq] at h
no goals
case neg.refine'_1.inr.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • ↑(-(π / 2))) = sign ↑(-(π / 2))
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
heq : toReal θ = -(π / 2)
⊢ False
simp at h
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (toReal (2 • θ)) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ False

case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ 2 • θ ≠ ↑π
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ False
rw [← sign_toReal hpi, _root_.sign_neg (hlt.trans (Left.neg_neg_iff.2 pi_div_two_pos)), ←
  sign_toReal] at h
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ 2 • θ ≠ ↑π

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

case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ 2 • θ ≠ ↑π
swap
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (toReal (2 • θ)) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -π / 2
⊢ False
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (toReal (2 • θ)) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ False
rw [← neg_div] at hlt
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 * π
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (toReal (2 • θ)) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -π / 2
⊢ False
rw [two_nsmul_toReal_eq_two_mul_add_two_pi.2 hlt.le, sign_pos] at h
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
he : 2 • θ = ↑π
⊢ False
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ 2 • θ ≠ ↑π
intro he
no goals
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
he : 2 • θ = ↑π
⊢ False
simp [he] at h
no goals
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : 1 = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -π / 2
⊢ False
simp at h
no goals
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 * π
linarith [neg_pi_lt_toReal θ]
case neg.refine'_2
θ : Angle
hpi : ¬θ = ↑π
h : -π / 2 < toReal θ ∧ toReal θ < π / 2
hpi' : 2 • θ ≠ ↑π
⊢ sign (2 • θ) = sign θ
case neg.refine'_2
θ : Angle
hpi : ¬θ = ↑π
h : abs (toReal θ) < π / 2
hpi' : 2 • θ ≠ ↑π
⊢ sign (2 • θ) = sign θ
rw [abs_lt, ← neg_div] at h
no goals
case neg.refine'_2
θ : Angle
hpi : ¬θ = ↑π
h : -π / 2 < toReal θ ∧ toReal θ < π / 2
hpi' : 2 • θ ≠ ↑π
⊢ sign (2 • θ) = sign θ
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]
θ : Angle
hpi : ¬θ = ↑π
h : abs (toReal θ) < π / 2
⊢ ¬θ = ↑(π / 2) ∧ ¬θ = ↑(-π / 2)
θ : Angle
hpi : ¬θ = ↑π
h : abs (toReal θ) < π / 2
⊢ 2 • θ ≠ ↑π
rw [Ne.def, two_nsmul_eq_pi_iff, not_or]
case left
θ : Angle
hpi : ¬θ = ↑π
h : abs (toReal θ) < π / 2
⊢ ¬θ = ↑(π / 2)

case right
θ : Angle
hpi : ¬θ = ↑π
h : abs (toReal θ) < π / 2
⊢ ¬θ = ↑(-π / 2)
θ : Angle
hpi : ¬θ = ↑π
h : abs (toReal θ) < π / 2
⊢ ¬θ = ↑(π / 2) ∧ ¬θ = ↑(-π / 2)
constructor
case left
hpi : ¬↑(π / 2) = ↑π
h : abs (toReal ↑(π / 2)) < π / 2
⊢ False
case left
θ : Angle
hpi : ¬θ = ↑π
h : abs (toReal θ) < π / 2
⊢ ¬θ = ↑(π / 2)
rintro rfl
no goals
case left
hpi : ¬↑(π / 2) = ↑π
h : abs (toReal ↑(π / 2)) < π / 2
⊢ False
simp [pi_pos, div_pos, abs_of_pos] at h
case right
hpi : ¬↑(-π / 2) = ↑π
h : abs (toReal ↑(-π / 2)) < π / 2
⊢ False
case right
θ : Angle
hpi : ¬θ = ↑π
h : abs (toReal θ) < π / 2
⊢ ¬θ = ↑(-π / 2)
rintro rfl
case right
hpi : ¬↑(-π / 2) = ↑π
h : abs (-π / 2) < π / 2
⊢ False
case right
hpi : ¬↑(-π / 2) = ↑π
h : abs (toReal ↑(-π / 2)) < π / 2
⊢ False
rw [toReal_neg_pi_div_two] at h
no goals
case right
hpi : ¬↑(-π / 2) = ↑π
h : abs (-π / 2) < π / 2
⊢ False
simp [pi_pos, div_pos, neg_div, abs_of_pos] at h