x : ℝ
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
x : ℝ
⊢ π / 4 ≤ arcsin x ↔ sqrt 2 / 2 ≤ x
rw [← sin_pi_div_four, le_arcsin_iff_sin_le']
x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
x : ℝ
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
have := pi_pos
no goals
x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
constructor <;> linarith