lean_workbook_plus_45770

Proved

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

Let $x\ ,\ y\in R$ such that $0 < y\le x\le 2\ ,\ xy^2 \le 2$ . Prove that $x + 2y\le 4$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45770 (x y : ℝ) (h₁ : 0 < y ∧ y ≤ x ∧ x ≤ 2) (h₂ : x * y ^ 2 ≤ 2) : x + 2 * y ≤ 4   :=  by sorry

Source