Prove2Me

lean_workbook_plus_52212

Open

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

For π<θ<3π2\pi < \theta < \frac{3\pi}{2} , sin(θ)<0sin(\theta) < 0 and cos(θ)<0cos(\theta) < 0 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52212 (θ : ℝ) (h₁ : π < θ) (h₂ : θ < 3 * π / 2) : sin θ < 0 ∧ cos θ < 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph