lean_workbook_plus_30555
ProvedSimplify the inequality to .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30555 (x : ℝ) : 9 * (x - 1) ^ 2 + 12 * x ≥ 8 * x ^ 2 ↔ (x - 3) ^ 2 ≥ 0 := by sorry
Source
Simplify the inequality to .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_30555 (x : ℝ) : 9 * (x - 1) ^ 2 + 12 * x ≥ 8 * x ^ 2 ↔ (x - 3) ^ 2 ≥ 0 := by sorry