lean_workbook_plus_72204

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Express $\cosh3t$ in terms of $\cosh t$ and simplify\n $\cosh3t=\cosh t\bigl(4\cosh^2t-3\bigl)=\cosh^3t\Bigl(4-\frac{3}{\cosh^2t}\Bigr)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72204 (t : ℝ) : Real.cosh (3 * t) = Real.cosh t * (4 * (Real.cosh t)^2 - 3)   :=  by sorry

Source