θ : Angle
⊢ toReal (2 • ↑(toReal θ)) = 2 * toReal θ + 2 * π ↔ toReal θ ≤ -π / 2
θ : Angle
⊢ toReal (2 • θ) = 2 * toReal θ + 2 * π ↔ toReal θ ≤ -π / 2
nth_rw 1 [← coe_toReal θ]
θ : Angle
⊢ -3 * π < 2 * toReal θ ∧ 2 * toReal θ ≤ -π ↔ toReal θ ≤ -π / 2
θ : Angle
⊢ toReal (2 • ↑(toReal θ)) = 2 * toReal θ + 2 * π ↔ toReal θ ≤ -π / 2
rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_add_two_pi_iff, Set.mem_Ioc]
no goals
θ : Angle
⊢ -3 * π < 2 * toReal θ ∧ 2 * toReal θ ≤ -π ↔ toReal θ ≤ -π / 2
refine'
  ⟨fun h => by linarith, fun h =>
    ⟨by linarith [pi_pos, neg_pi_lt_toReal θ], (le_div_iff' (zero_lt_two' ℝ)).1 h⟩⟩
no goals
θ : Angle
h : -3 * π < 2 * toReal θ ∧ 2 * toReal θ ≤ -π
⊢ toReal θ ≤ -π / 2
linarith
no goals
θ : Angle
h : toReal θ ≤ -π / 2
⊢ -3 * π < 2 * toReal θ
linarith [pi_pos, neg_pi_lt_toReal θ]