Prove2Me

Lean-Workbook Plus 80535: Trigonometric identity

Proved
WorkbookRestored.plus_80535

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For every real bb, there exists a real rbr_b such that sin⁡rb=1/1+b2\sin r_b=1/\sqrt{1+b^2}.

Source: Lean-Workbook row lean_workbook_plus_80535 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
open Real
Formal statement
theorem WorkbookRestored.plus_80535 (b : ℝ) : ∃ r_b, sin r_b = 1 / Real.sqrt (1 + b^2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_80535; immutable original Prove2Me node b645f6a3-7565-48ee-8898-cf16363a3c51

View graph