x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
x y : ℂ
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
have h1 : x + 2 * x = 3 * x := by ring
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * cosh x ^ 3 - 3 * cosh x
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
rw [← h1, cosh_add x (2 * x)]
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * cosh x ^ 3 - 3 * cosh x
simp only [cosh_two_mul, sinh_two_mul]
x y : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x
have h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2 := by ring
x y : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + (cosh x ^ 2 - 1)) + 2 * cosh x * (cosh x ^ 2 - 1) = 4 * cosh x ^ 3 - 3 * cosh x
x y : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x
rw [h2, sinh_sq]
no goals
x y : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + (cosh x ^ 2 - 1)) + 2 * cosh x * (cosh x ^ 2 - 1) = 4 * cosh x ^ 3 - 3 * cosh x
ring
no goals
x y : ℂ
⊢ x + 2 * x = 3 * x
ring
no goals
x y : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
ring