lean_workbook_plus_55323

Proved

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

Determine the validity of the statement 'If $a^5 - a^3 + a = 2$ and $a > 0$ , then $a^3 \leq 2$ .'

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55323 (a : ℝ) (h₁ : a > 0) (h₂ : a^5 - a^3 + a = 2) : a^3 ≤ 2   :=  by sorry

Source