lean_workbook_plus_39773

Proved

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

If $x,y$ be be nonnegative real numbers such that $x+y^{2}\geq x^{2}+y^{3}$ , then $3x^{2}+2y^{3}\leq5$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39773 (x y : ℝ) (hx: x >= 0 ∧ y >= 0) (h : x + y^2 >= x^2 + y^3): 3 * x^2 + 2 * y^3 <= 5   :=  by sorry

Source