English
Let x and y be complex numbers such that neither is an odd multiple of π/2. Then tan(x+y) equals (tan x + tan y) divided by (1 − tan x tan y).
Русский
Пусть x и y — комплексные числа, ни одно из которых не является нечетным кратным π/2. Тогда tan(x+y) = (tan x + tan y) / (1 − tan x tan y).
LaTeX
$$$$\\tan(x+y) = \\frac{\\tan x + \\tan y}{1 - \\tan x \\tan y}$$$$
Lean4
theorem tan_add {x y : ℂ}
(h :
((∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, y ≠ (2 * l + 1) * π / 2) ∨
(∃ k : ℤ, x = (2 * k + 1) * π / 2) ∧ ∃ l : ℤ, y = (2 * l + 1) * π / 2) :
tan (x + y) = (tan x + tan y) / (1 - tan x * tan y) :=
by
rcases h with (⟨h1, h2⟩ | ⟨⟨k, rfl⟩, ⟨l, rfl⟩⟩)
· rw [tan, sin_add, cos_add, ←
div_div_div_cancel_right₀ (mul_ne_zero (cos_ne_zero_iff.mpr h1) (cos_ne_zero_iff.mpr h2)), add_div, sub_div]
simp only [← div_mul_div_comm, tan, mul_one, one_mul, div_self (cos_ne_zero_iff.mpr h1),
div_self (cos_ne_zero_iff.mpr h2)]
· haveI t := tan_int_mul_pi_div_two
obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))
simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one] at hx hy hxy
rw [hx, hy, add_zero, zero_div, mul_div_assoc, mul_div_assoc, ← add_mul (2 * (k : ℂ) + 1) (2 * l + 1) (π / 2), ←
mul_div_assoc, hxy]
