Lean-Workbook Plus 18380: Trigonometric inequality

Proved

WorkbookRestored.plus_18380

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

lean-workbookrestored-importssource-checked

If $a,b$ are real and $a^2+b^2=1$ , then $a\sin x+b\cos x\le1$ for every real $x$ . This proves the upper-bound component of the source maximum-value statement.

Source: Lean-Workbook row lean_workbook_plus_18380 (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_18380 (a b : ℝ) (x : ℝ) (h : a^2 + b^2 = 1) :
  a * Real.sin x + b * Real.cos x ≤ 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_18380; immutable original Prove2Me node f634a1cb-446e-4e53-ba41-35236b0bb682

View graph