lean_workbook_plus_71724

Proved

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

Let $x,y \in \mathbb{R}$ such that $x+y = 2$ . Prove that $xy(x^2+y^2) \le 2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71724 (x y : ℝ) (h : x + y = 2) : x * y * (x ^ 2 + y ^ 2) ≤ 2   :=  by sorry

Source