lean_workbook_plus_33683
OpenProve that:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33683 (A B C : ℝ) : (sin A + sin B + sin C) ^ 2 ≤ 3 * (sin A ^ 2 + sin B ^ 2 + sin C ^ 2) := by sorry
Source
Prove that:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_33683 (A B C : ℝ) : (sin A + sin B + sin C) ^ 2 ≤ 3 * (sin A ^ 2 + sin B ^ 2 + sin C ^ 2) := by sorry