lean_workbook_plus_14542

Proved

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

$ab+c(a+b)=9$ we see that $a,b$ satisfy $a+b=6-c$ and $ab=(c-3)^2$ so $a$ and $b$ are the roots of $f(x)=x^2+(c-6)x+(c-3)^2=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14542  (a b c : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = x^2 + (c - 6) * x + (c - 3)^2)
  (h₁ : f a = 0)
  (h₂ : f b = 0)
  (h₃ : a + b = 6 - c)
  (h₄ : a * b = (c - 3)^2) :
  9 = a * b + c * (a + b)   :=  by sorry

Source

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

View graph