θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ sin ↑θ
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ sign ↑θ
rw [sign, sign_nonneg_iff]
no goals
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ sin ↑θ
exact sin_nonneg_of_nonneg_of_le_pi h0 hpi