lean_workbook_plus_60494

Open

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

Prove that $\log \left ( \tan \left ( \frac{\pi}{4}-a \right ) \right ) =-\log \left ( \tan \left ( \frac{\pi}{4}+a \right ) \right )$ for $0<a<\frac{\pi}{4}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60494 (a : ℝ) (ha : 0 < a ∧ a < Real.pi / 4) : Real.log (Real.tan (Real.pi / 4 - a)) = -Real.log (Real.tan (Real.pi / 4 + a))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph