x : ℝ
h : 0 ≤ x
⊢ arcsin (x / sqrt (↑1 + x ^ 2)) = arcsin (sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2))

x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (sqrt (↑1 + x ^ 2))⁻¹
x : ℝ
h : 0 ≤ x
⊢ arctan x = arccos (sqrt (↑1 + x ^ 2))⁻¹
rw [arctan_eq_arcsin, arccos_eq_arcsin]
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (sqrt (↑1 + x ^ 2))⁻¹

x : ℝ
h : 0 ≤ x
⊢ arcsin (x / sqrt (↑1 + x ^ 2)) = arcsin (sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2))
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / sqrt (↑1 + x ^ 2)) = arcsin (sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2))

x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (sqrt (↑1 + x ^ 2))⁻¹
swap
case e_a
x : ℝ
h : 0 ≤ x
⊢ x / sqrt (↑1 + x ^ 2) = sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2)
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / sqrt (↑1 + x ^ 2)) = arcsin (sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2))
congr 1
case e_a.hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2

case e_a
x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0

case e_a
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹
case e_a
x : ℝ
h : 0 ≤ x
⊢ x / sqrt (↑1 + x ^ 2) = sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2)
rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel', sqrt_div, sqrt_sq h]
no goals
case e_a.hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2

case e_a
x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0

case e_a
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹
all_goals positivity
no goals
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (sqrt (↑1 + x ^ 2))⁻¹
exact inv_nonneg.2 (sqrt_nonneg _)
no goals
case e_a
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹
positivity