English
Let x and y be complex numbers with the usual domain restrictions. Then tan(x−y) equals (tan x − tan y) divided by (1 + tan x tan y).
Русский
Пусть x и y — комплексные числа с обычными ограничениями области. Тогда 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_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
have :=
tan_add (x := x) (y := -y) <| by
rcases h with ⟨x_ne, minus_y_ne⟩ | ⟨x_eq, minus_y_eq⟩
· refine .inl ⟨x_ne, fun l => ?_⟩
rw [Ne, neg_eq_iff_eq_neg]
convert minus_y_ne (-l - 1) using 2
push_cast
ring
· refine .inr ⟨x_eq, ?_⟩
rcases minus_y_eq with ⟨l, rfl⟩
use -l - 1
push_cast
ring
rw [tan_neg] at this
convert this using 2
ring
