Prove2Me

Lean-Workbook Plus 25423: Trigonometric inequality

Proved
WorkbookRestored.plus_25423

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

lean-workbookrestored-importssource-checked

For real x,yx,y, tan⁡4x+tan⁡4y≥2tan⁡2xtan⁡2y\tan^4x+\tan^4y\ge2\tan^2x\tan^2y.

Source: Lean-Workbook row lean_workbook_plus_25423 (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_25423 (x y : ℝ) : tan x ^ 4 + tan y ^ 4 ≥ 2 * tan x ^ 2 * tan y ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_25423; immutable original Prove2Me node 9786711d-b0ea-4a5c-bdc2-bde4d2989715

View graph