x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x
x : ℝ
hx : x ∈ Icc 0 π
⊢ 0 ≤ sin x
rw [← closure_Ioo pi_ne_zero.symm] at hx
no goals
x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x
exact
  closure_lt_subset_le continuous_const continuous_sin
    (closure_mono (fun y => sin_pos_of_mem_Ioo) hx)