lean_workbook_plus_72895

Proved

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

Let the two numbers be $x$ and $y$ . Then $x+y=4xy,$ so the sum of their reciprocals is $\displaystyle\frac{1}{x}+\displaystyle\frac{1}{y}=\displaystyle\frac{x+y}{xy}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72895  (x y : ℝ)
  (h₀ : x + y = 4 * (x * y))
  (h₁ : x ≠ 0 ∧ y ≠ 0) :
  1 / x + 1 / y = (x + y) / (x * y)   :=  by sorry

Source

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

View graph