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