Prove2Me

An identity under a positive unit-product constraint

Proved
WorkbookSource.problem_47734

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let x,y,z∈R+x,y,z\in R^+ such that xyz=1 xyz=1 . Prove that

(x+1x−zy)2+\left(x+\frac{1}{x}-\frac{z}{y}\right)^2+ (y+1y−xz)2+\left(y+\frac{1}{y}-\frac{x}{z}\right)^2+ (z+1z−yx)2+\left(z+\frac{1}{z}-\frac{y}{x}\right)^2+ (x+1x−zy)(y+1y−xz)(z+1z−yx)=4\left(x+\frac{1}{x}-\frac{z}{y}\right) \left(y+\frac{1}{y}-\frac{x}{z}\right) \left(z+\frac{1}{z}-\frac{y}{x}\right)=4 .

Source: InternLM Lean-Workbook, record lean_workbook_47734 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_47734 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (h : x * y * z = 1) : (x + 1 / x - z / y)^2 + (y + 1 / y - x / z)^2 + (z + 1 / z - y / x)^2 + (x + 1 / x - z / y) * (y + 1 / y - x / z) * (z + 1 / z - y / x) = 4  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_47734; Apache-2.0

View graph