lean_workbook_plus_58924

Proved

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

Suppose that positive numbers $x$ and $y$ satisfy $x^{2}+2y^{3}-y^{4}\leq \frac{2x^{3}+1}{3}+2y^{3}-\frac{4y^{3}-1}{3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58924 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : x^2 + 2*y^3 - y^4 ≤ (2*x^3 + 1)/3 + 2*y^3 - (4*y^3 - 1)/3   :=  by sorry

Source