Prove2Me

Lean-Workbook Plus 46535: Trigonometric inequality

Proved
WorkbookRestored.plus_46535

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

lean-workbookrestored-importssource-checked

For 0<x<π0<x<\pi, (9x2sin⁡2x+4)/(xsin⁡x)≥12(9x^2\sin^2x+4)/(x\sin x)\ge12. This is the lower-bound component of the source’s minimum-value problem.

Source: Lean-Workbook row lean_workbook_plus_46535 (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_46535 (x : ℝ) (hx : 0 < x ∧ x < π) : (9 * (x ^ 2 * (sin x) ^ 2) + 4) / (x * sin x) ≥ 12   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_46535; immutable original Prove2Me node 3e7d89b6-def1-44be-9d34-782b41d99fa9

View graph