x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x
x : ℝ
h : 0 ≤ x
⊢ arcsin x = arccos (sqrt (1 - x ^ 2))
rw [eq_comm, ← cos_arcsin]
no goals
x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x
exact
  arccos_cos (arcsin_nonneg.2 h)
    ((arcsin_le_pi_div_two _).trans (div_le_self pi_pos.le one_le_two))