lean_workbook_plus_26233

Proved

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

Prove that for all $t \in [0, 1)$ , the inequality $\frac{3(1 + t)(1 - 2t)^2 t^2}{(1 + 2t)(1 - t)} \ge 0$ holds.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26233 (t : ℝ) (ht : t ∈ Set.Ico (0 : ℝ) 1) : (3 * (1 + t) * (1 - 2 * t) ^ 2 * t ^ 2) / (1 + 2 * t) / (1 - t) ≥ 0   :=  by sorry

Source

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

View graph