θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ sin ↑θ
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ sign (-↑θ) ≤ 0
rw [sign, sign_nonpos_iff, sin_neg, Left.neg_nonpos_iff]
no goals
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ sin ↑θ
exact sin_nonneg_of_nonneg_of_le_pi h0 hpi