Prove2Me

Lean-Workbook Plus 72204: Trigonometric identity

Proved
WorkbookRestored.plus_72204

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For real tt, cosh⁡(3t)=cosh⁡t(4cosh⁡2t−3)\cosh(3t)=\cosh t(4\cosh^2t-3). This is the first identity in the source.

Source: Lean-Workbook row lean_workbook_plus_72204 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real
Formal statement
theorem WorkbookRestored.plus_72204 (t : ℝ) : Real.cosh (3 * t) = Real.cosh t * (4 * (Real.cosh t)^2 - 3)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_72204; immutable original Prove2Me node a0914547-1841-4195-b785-7a25f0b1472a

View graph