From 1a2eb0b514cc0c2ceab745caa4d810244984fa8d Mon Sep 17 00:00:00 2001
From: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
Date: Thu, 4 Feb 2021 12:05:37 +0000
Subject: [PATCH] feat(analysis/special_functions/trigonometric): add
 mistakenly omitted lemma (#6036)

---
 src/analysis/special_functions/trigonometric.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/analysis/special_functions/trigonometric.lean b/src/analysis/special_functions/trigonometric.lean
index 0b31df80d84b1..f38f986433abb 100644
--- a/src/analysis/special_functions/trigonometric.lean
+++ b/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]