Prove2Me

A quadratic bound from a determinant constraint

Proved
WorkbookSource.problem_43314

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

If real numbers x,y,zx,y,z satisfy xy−z2≥1xy-z^2\ge1, then

(x+2y)2≥(y+2z)2+6.(x+2y)^2\ge(y+2z)^2+6.

Source: InternLM Lean-Workbook, record lean_workbook_43314 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_43314 (x y z : ℝ) (h : 1 ≤ x*y - z^2) : (x + 2*y)^2 ≥ (y + 2*z)^2 + 6  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_43314; Apache-2.0

View graph