no goals
x : ℝ
h : x ∈ Ioo (-1) 1
⊢ arcsin x = arctan (x / sqrt (↑1 - x ^ 2))
rw_mod_cast [arctan_eq_arcsin, div_pow, sq_sqrt, one_add_div, div_div, ← sqrt_mul,
  mul_div_cancel', sub_add_cancel, sqrt_one, div_one] <;> simp at h <;> nlinarith [h.1, h.2]