lean_workbook_plus_79716

Proved

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

Let $x,y$ be positive real numbers such that $x+2y=8$ . Prove that

\left(x+\dfrac{1}{y}\right)\left(y+\dfrac{1}{x}\right){\geq}4

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79716 (x y : ℝ) (hx : x > 0) (hy : y > 0) (hxy : x + 2 * y = 8) : (x + 1 / y) * (y + 1 / x) ≥ 4   :=  by sorry

Source