lean_workbook_plus_22143

Proved

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

Prove that $x+y+z\leqslant 6$ given $x,y,z\in R, 0<x\leq y\leq z\leq 3. yz\leq 6, xyz\leq 6.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_22143 (x y z : ℝ) (hxy : 0 < x ∧ x ≤ y) (hyz : y ≤ z ∧ z ≤ 3) (h : y * z ≤ 6) (h' : x * y * z ≤ 6) : x + y + z ≤ 6   :=  by sorry

Source

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

View graph