English
If z is not equal to π/2 and its real part lies in (-π/2, π/2], then arctan(tan z) = z.
Русский
Если z ≠ π/2 и Re z ∈ (-π/2, π/2], то arctan(tan z) = z.
LaTeX
$$$\\arctan(\\tan z) = z \\quad\\text{ under } z \\ne \\frac{\\pi}{2},\\; -\\frac{\\pi}{2} < \\Re z ≤ \\frac{\\pi}{2}.$$$
Lean4
theorem arctan_tan {z : ℂ} (h₀ : z ≠ π / 2) (h₁ : -(π / 2) < z.re) (h₂ : z.re ≤ π / 2) : arctan (tan z) = z :=
by
have h := cos_ne_zero_of_arctan_bounds h₀ h₁ h₂
unfold arctan tan
rw [← mul_div_mul_right (1 + _) _ h, add_mul, sub_mul, one_mul, ← mul_rotate, mul_div_cancel₀ _ h]
conv_lhs =>
enter [2, 1, 2]
rw [sub_eq_add_neg, ← neg_mul, ← sin_neg, ← cos_neg]
rw [← exp_mul_I, ← exp_mul_I, ← exp_sub, show z * I - -z * I = 2 * (I * z) by ring, log_exp,
show -I / 2 * (2 * (I * z)) = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
all_goals norm_num
· rwa [← div_lt_iff₀' two_pos, neg_div]
· rwa [← le_div_iff₀' two_pos]
