lean_workbook_plus_33208

Open

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

Denote $\sin(x)=y, \cos(x)=z$ . Then $y^2+z^2=1$ and we have $y^2+3yz-15z^2=0$ and hence $9y^2z^2=(15z^2-y^2)^2$ or, equivalently $9y^2(1-y^2)=(16y^2-15)^2$ which resolves to $265y^4-489y^2+225=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33208  (x : ℝ)
  (y z : ℝ)
  (h₀ : sin x = y)
  (h₁ : cos x = z)
  (h₂ : y^2 + z^2 = 1)
  (h₃ : y^2 + 3 * y * z - 15 * z^2 = 0) :
  9 * y^2 * (1 - y^2) = (16 * y^2 - 15)^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph