English
For all z ≠ i and z ≠ -i, tan(arctan z) = z.
Русский
Для всех z, отличных от i и -i, tan(arctan z) = z.
LaTeX
$$$\\tan(\\arctan z) = z\\quad\\text{ if } z \\neq i, \\ z \\neq -i.$$$
Lean4
theorem tan_arctan {z : ℂ} (h₁ : z ≠ I) (h₂ : z ≠ -I) : tan (arctan z) = z :=
by
unfold tan sin cos
rw [div_div_eq_mul_div, div_mul_cancel₀ _ two_ne_zero, ← div_mul_eq_mul_div,
-- multiply top and bottom by `exp (arctan z * I)`
← mul_div_mul_right _ _ (exp_ne_zero (arctan z * I)), sub_mul, add_mul, ← exp_add, neg_mul, neg_add_cancel,
exp_zero, ← exp_add, ← two_mul]
have z₁ : 1 + z * I ≠ 0 := by
contrapose! h₁
rw [add_eq_zero_iff_neg_eq, ← div_eq_iff I_ne_zero, div_I, neg_one_mul, neg_neg] at h₁
exact h₁.symm
have z₂ : 1 - z * I ≠ 0 := by
contrapose! h₂
rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂
exact h₂.symm
have key : exp (2 * (arctan z * I)) = (1 + z * I) / (1 - z * I) :=
by
rw [arctan, ← mul_rotate, ← mul_assoc, show 2 * (I * (-I / 2)) = 1 by simp [field], one_mul, exp_log]
· exact div_ne_zero z₁ z₂
rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
