Prove2Me

lean_workbook_plus_77082

Open

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

A slightly more rigorous approach would be to start with sin⁡2xcos⁡x\frac{\sin 2x}{\cos x} as an expression, and not start with an equality. Transform that via the double angle identity for sine into 2sin⁡xcos⁡xcos⁡x\frac{2\sin x \cos x}{\cos x} . Then, cancel the cosines (noting that we now have forced the issue of cos⁡x≠0\cos x \neq 0 ) to get 2sin⁡x2\sin x . That's your RHS.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77082  (x : ℝ)
  (h₀ : cos x ≠ 0) :
  sin (2 * x) / cos x = 2 * sin x   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph