lean_workbook_plus_4325

Proved

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

Let $x, y \in \mathbb{R}$ and $| 2x-y |\le 3$ and $| x-3y | \le 1$ . Find maximum value of $P=x^2+xy+y^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4325 (x y : ℝ) (h1 : abs (2*x - y) ≤ 3) (h2 : abs (x - 3*y) ≤ 1) : x^2 + x*y + y^2 ≤ 7   :=  by sorry

Source