by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
I beg to differ. From (the edited) m=cos6x+sin6x=(cos2x+sin2x)(cos4x−cos2xsin2x+sin4x)=(cos2x+sin2x)2−3cos2xsin2x=1−43sin22x follows 41≤m≤1 , since 0≤sin22x≤1 (the value 47 was incorrectly obtained assuming we might have sin22x=−1 ).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13487 :
∀ x : ℝ, 1 / 4 ≤ cos x ^ 6 + sin x ^ 6 ∧ cos x ^ 6 + sin x ^ 6 ≤ 1 := by sorry