lean_workbook_plus_24283

Open

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

Prove that in any triangle with angles A, B, and C, the following equation holds:\n$\sin^2A + \sin^2B + \sin^2C = 2(1 + \cosA \cosB \cosC)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24283 (A B C : ℝ) (hx: A + B + C = π) : (sin A)^2 + (sin B)^2 + (sin C)^2 = 2*(1 + cos A * cos B * cos C)   :=  by sorry

Source