Prove2Me

lean_workbook_plus_59083

Proved

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

Let x1>x2>0x_1 > x_2>0 , then f(x1)−f(x2)=x1−x2+1x1−1x2=(x1−x2)(x1x2−1)x1x2f(x_1)-f(x_2)=x_1-x_2+\dfrac{1}{x_1}-\dfrac{1}{x_2}=\dfrac{(x_1-x_2)(x_1x_2-1)}{x_1x_2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59083  (x1 x2 : ℝ)
  (h₀ : 0 < x1 ∧ 0 < x2)
  (h₁ : x1 > x2) :
  x1 - x2 + (1 / x1 - 1 / x2) = (x1 - x2) * (x1 * x2 - 1) / (x1 * x2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph