English
Let x,y ∈ ℝ be such that neither x nor y is an odd multiple of π/2, or both are such multiples appropriately; then tan(x+y) = (tan x + tan y) / (1 − tan x tan y).
Русский
Пусть x,y ∈ ℝ таковы, что либо ни одно из них не является нечетной кратной π/2, либо оба являются такими кратностями; тогда tan(x+y) = (tan x + tan y) / (1 − tan x tan y).
LaTeX
$$$ \Big(\big( \forall k \in \mathbb{Z}, x \neq (2k+1) \frac{\pi}{2} \big) \land \big( \forall l \in \mathbb{Z}, y \neq (2l+1) \frac{\pi}{2} \big)\Big) \\ \lor \\ \Big(\exists k \in \mathbb{Z}, x = (2k+1) \frac{\pi}{2} \land \exists l \in \mathbb{Z}, y = (2l+1) \frac{\pi}{2}\Big) \\ : \\ tan(x+y) = \frac{\tan x + \tan y}{1 - \tan x \tan y} $$$
Lean4
theorem tan_add
(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
simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_div, Complex.ofReal_mul,
Complex.ofReal_tan] using @Complex.tan_add (x : ℂ) (y : ℂ) (by convert h <;> norm_cast)
