lean_workbook_plus_31883

Proved

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

Now what we need to prove is just $(1+t)^2 \ge 12(t-2)$ , or $t^2-10t+25 \ge 0$ , which is just $(t-5)^2 \ge 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31883 : ∀ t : ℝ, (1 + t) ^ 2 ≥ 12 * (t - 2)   :=  by sorry

Source