Prove2Me

lean_workbook_plus_26813

Proved

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

Given ∑cyc11+a2=2\sum_{cyc} \frac {1}{1+a^2} = 2, show that ∑a2a2+1=1\sum \frac{a^2}{a^2+1} = 1.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_26813 (a b c : ℝ) (h : 1 / (1 + a ^ 2) + 1 / (1 + b ^ 2) + 1 / (1 + c ^ 2) = 2) :
  a ^ 2 / (a ^ 2 + 1) + b ^ 2 / (b ^ 2 + 1) + c ^ 2 / (c ^ 2 + 1) = 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph