x : ℝ
this : Complex.tan (2 * ↑x) = 2 * Complex.tan ↑x / (1 - Complex.tan ↑x ^ 2)
⊢ tan (2 * x) = ↑2 * tan x / (↑1 - tan x ^ 2)
x : ℝ
⊢ tan (2 * x) = ↑2 * tan x / (↑1 - tan x ^ 2)
have := @Complex.tan_two_mul x
no goals
x : ℝ
this : Complex.tan (2 * ↑x) = 2 * Complex.tan ↑x / (1 - Complex.tan ↑x ^ 2)
⊢ tan (2 * x) = ↑2 * tan x / (↑1 - tan x ^ 2)
norm_cast at *