English
Let x ≥ 0. Then arctan x equals arccos(1/√(1+x^2)).
Русский
Пусть x ≥ 0. Тогда arctan x равно arccos(1/√(1+x^2)).
LaTeX
$$$\\\\arctan x = \\\\arccos\\\\left(\\\\frac{1}{\\\\sqrt{1+x^2}}\\\\right), \\\\quad x \ge 0.$$$
Lean4
theorem arctan_eq_arccos (h : 0 ≤ x) : arctan x = arccos (√(1 + x ^ 2))⁻¹ :=
by
rw [arctan_eq_arcsin, arccos_eq_arcsin]; swap; · exact inv_nonneg.2 (sqrt_nonneg _)
congr 1
rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel_left, sqrt_div, sqrt_sq h]
all_goals
positivity
-- The junk values for `arccos` and `sqrt` make this true even for `1 < x`.