Prove2Me

Lean-Workbook Plus 19270: Trigonometric identity

Proved
WorkbookRestored.plus_19270

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

lean-workbookrestored-importssource-checked

If sin⁡x≠0\sin x\ne0 and cos⁡x≠0\cos x\ne0, then tan⁡x+1/tan⁡x=1/(sin⁡xcos⁡x)\tan x+1/\tan x=1/(\sin x\cos x).

Source: Lean-Workbook row lean_workbook_plus_19270 (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
open Real
Formal statement
theorem WorkbookRestored.plus_19270 (x : ℝ) (hx : sin x ≠ 0 ∧ cos x ≠ 0) : tan x + 1 / tan x = 1 / (sin x * cos x)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_19270; immutable original Prove2Me node cb9c721a-ae5b-405c-ad8b-ecb20a83a0f2

View graph