lean_workbook_plus_194

Proved

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

The area of the rectangle is $2x(9-x^2)$ , where x is positive, since the dimensions are $2x$ in width and $9-x^2$ in height. We are given that it is equal to 20. Therefore, $x(9-x^2)=10$ , and $x^3-9x+10=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_194 (x : ℝ) (hx : x > 0) (h : x * (9 - x^2) = 10) : x^3 - 9 * x + 10 = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph