lean_workbook_plus_19270

Open

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

$\tan{x}+\cot{x}=\frac{\sin{x}}{\cos{x}}+\frac{\cos{x}}{\sin{x}}=\frac{1}{\sin{x}\cos{x}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19270 (x : ℝ) (hx : sin x ≠ 0 ∧ cos x ≠ 0) : tan x + 1 / tan x = 1 / (sin x * cos x)   :=  by sorry

Source