Prove2Me

lean_workbook_plus_48585

Proved

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

so f(tan⁡ξ)(1+tan⁡2ξ)=1{\mathop{\rm f}\nolimits} (\tan \xi )(1 + \tan ^2 \xi ) = 1 ⇒f(tan⁡ξ)=11+tan⁡2ξ \Rightarrow \mathop {}\limits^{} {\mathop{\rm f}\nolimits} (\tan \xi ) = \frac{1}{{1 + \tan ^2 \xi }}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48585 tan_eq_v (f : ℝ → ℝ) : f tan_eq_v * (1 + tan_eq_v^2) = 1 → f tan_eq_v = 1 / (1 + tan_eq_v^2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph