lean_workbook_plus_82516

Proved

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

Solution 2.\na=k\frac{x}{y},b=k\frac{y}{z},c=k\frac{z}{x}.\n $\frac{1}{a(b+1)}+\frac{1}{b(c+1)}+\frac{1}{c(a+1)}=\frac{yz}{kx(ky+z)}+\frac{zx}{ky(kz+x)}+\frac{xy}{kz(kx+y)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82516 (x y z k a b c : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) (hab : a = k * x / y) (hbc : b = k * y / z) (hca : c = k * z / x) : 1 / (a * (b + 1)) + 1 / (b * (c + 1)) + 1 / (c * (a + 1)) = (y * z) / (k * x * (k * y + z)) + (z * x) / (k * y * (k * z + x)) + (x * y) / (k * z * (k * x + y))   :=  by sorry

Source

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

View graph