x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3
x y : ℂ
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3
have h1 : x + 2 * x = 3 * x := by ring
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin x * cos (2 * x) + cos x * sin (2 * x) = 3 * sin x - 4 * sin x ^ 3
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3
rw [← h1, sin_add x (2 * x)]
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin x * cos (2 * x) + cos x * sin (2 * x) = 3 * sin x - 4 * sin x ^ 3
simp only [cos_two_mul, sin_two_mul, cos_sq']
x y : ℂ
h1 : x + 2 * x = 3 * x
h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3
have h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2 := by ring
x y : ℂ
h1 : x + 2 * x = 3 * x
h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + 2 * sin x * (1 - sin x ^ 2) = 3 * sin x - 4 * sin x ^ 3
x y : ℂ
h1 : x + 2 * x = 3 * x
h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + cos x * (2 * sin x * cos x) = 3 * sin x - 4 * sin x ^ 3
rw [h2, cos_sq']
no goals
x y : ℂ
h1 : x + 2 * x = 3 * x
h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2
⊢ sin x * (2 * (1 - sin x ^ 2) - 1) + 2 * sin x * (1 - sin x ^ 2) = 3 * sin x - 4 * sin x ^ 3
ring
no goals
x y : ℂ
⊢ x + 2 * x = 3 * x
ring
no goals
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2
ring