English
Let x,y ∈ ℝ satisfy the standard non-singularity condition; then tan(x−y) = (tan x − tan y)/(1 + tan x tan y).
Русский
Пусть x,y∈ℝ удовлетворяют обычному условию невозмездности синуса; тогда 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) \\Rightarrow \ tan(x-y) = \frac{\tan x - \tan y}{1 + \tan x \tan y} $$$
Lean4
theorem tan_sub {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
simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_div, Complex.ofReal_mul,
Complex.ofReal_tan] using @Complex.tan_sub (x : ℂ) (y : ℂ) (by convert h <;> norm_cast)
