x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
x : ℝ
⊢ arccos x ≤ π / 4 ↔ sqrt 2 / 2 ≤ x
rw [arccos, ← pi_div_four_le_arcsin]
case mpr
x : ℝ
a✝ : π / 4 ≤ arcsin x
⊢ π / 2 - arcsin x ≤ π / 4
case mpr
x : ℝ
⊢ π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4
intro
no goals
case mpr
x : ℝ
a✝ : π / 4 ≤ arcsin x
⊢ π / 2 - arcsin x ≤ π / 4
linarith