Prove2Me

lean_workbook_plus_31096

Open

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

prove that cos(A−B)+cos(B−C)+cos(C−A)≤3 cos(A-B)+cos(B-C)+cos(C-A) \leq 3

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_31096 (A B C : ℝ) : Real.cos (A - B) + Real.cos (B - C) + Real.cos (C - A) ≤ 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph