lean_workbook_plus_80965

Proved

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

Given $(a+1)(b+1)(c+1)=8$ and $a,b,c \geq 0$ , prove that $abc \leq 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80965 (a b c : ℝ) (h : a ≥ 0 ∧ b ≥ 0 ∧ c ≥ 0) (h1 : (a + 1) * (b + 1) * (c + 1) = 8) : a * b * c ≤ 1   :=  by sorry

Source