lean_workbook_plus_12925

Proved

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

prove that $6t^5-15t^4+6t^3+6t^2-4t+1 \ge 0$ for $0 \le t \le 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12925 (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 6 * t ^ 5 - 15 * t ^ 4 + 6 * t ^ 3 + 6 * t ^ 2 - 4 * t + 1 ≥ 0   :=  by sorry

Source