lean_workbook_plus_71483

Open

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

Given that $Cosx = Cosy$ and $Sinx = -Siny$ , Show that $Sin^2 \frac {x + y}{2} = 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71483 (x y : ℝ) (h₁ : Real.cos x = Real.cos y) (h₂ : Real.sin x = -Real.sin y) : (Real.sin ((x + y) / 2))^2 = 0   :=  by sorry

Source

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

View graph