lean_workbook_plus_32507

Open

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

Prove that: $sin(B)^2+sin(C)^2=1+cos(A)cos(B)cos(C)+cos(A)sin(B)sin(C)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32507 (A B C : ℝ) (hA : A = π - (B + C)) (hB : 0 < B ∧ 0 < C) (hC : 0 < A ∧ 0 < B ∧ 0 < C) : sin B ^ 2 + sin C ^ 2 = 1 + cos A * cos B * cos C + cos A * sin B * sin C   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph