Prove2Me

lean_workbook_plus_31707

Proved

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

assume , b≤max(a,c) b \leq max(a,c) and b≥min(a,c) b \geq min(a,c) \n =>a(b−a)(b−c)≤0  ⟺  a2b+abc≥ab2+ca2(1) = > a(b - a)(b - c) \leq 0 \iff a^2b + abc \geq ab^2 + ca^2 (1)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_31707  (a b c : ℝ)
  (h₀ : b ≤ max a c)
  (h₁ : b ≥ min a c) :
  a * (b - a) * (b - c) ≤ 0 ↔ a^2 * b + a * b * c ≥ a * b^2 + c * a^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph