x : ℝ
h : 0 < x
⊢ arctan (sqrt (↑1 - x ^ 2) / x) = π / 2 - arcsin x
x : ℝ
h : 0 < x
⊢ arccos x = arctan (sqrt (↑1 - x ^ 2) / x)
rw [arccos, eq_comm]
case refine'_1
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = sqrt (↑1 - x ^ 2) / x

case refine'_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x

case refine'_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2
x : ℝ
h : 0 < x
⊢ arctan (sqrt (↑1 - x ^ 2) / x) = π / 2 - arcsin x
refine' arctan_eq_of_tan_eq _ ⟨_, _⟩
no goals
case refine'_1
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = sqrt (↑1 - x ^ 2) / x
rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]
no goals
case refine'_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x
linarith only [arcsin_le_pi_div_two x, pi_pos]
no goals
case refine'_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2
linarith only [arcsin_pos.2 h]