feat(analysis/special_functions/trigonometric): add mistakenly omitte…

…d lemma (#6036)

src/analysis/special_functions/trigonometric.lean

@@ -2797,6 +2797,14 @@ lemma neg_pi_div_two_lt_arctan (x : ℝ) : -(π / 2) < arctan x :=
 lemma arctan_eq_arcsin (x : ℝ) : arctan x = arcsin (x / sqrt (1 + x ^ 2)) :=
 eq.symm $ arcsin_eq_of_sin_eq (sin_arctan x) (mem_Icc_of_Ioo $ arctan_mem_Ioo x)
 
+lemma arcsin_eq_arctan {x : ℝ} (h : x ∈ Ioo (-(1:ℝ)) 1) :
+  arcsin x = arctan (x / sqrt (1 - x ^ 2)) :=
+begin
+  rw [arctan_eq_arcsin, div_pow, sqr_sqrt, one_add_div, div_div_eq_div_mul,
+      ← sqrt_mul, mul_div_cancel', sub_add_cancel, sqrt_one, div_one];
+  nlinarith [h.1, h.2],
+end
+
 @[simp] lemma arctan_zero : arctan 0 = 0 :=
 by simp [arctan_eq_arcsin]