lean_workbook_plus_34495Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)a,b,c,d≥0a,b,c,d\geq 0a,b,c,d≥0 \n \n (2+a+c)2(2+b+d)2≥16 (1+a)(1+b)(1+c)(1+d)\left( 2+a+c \right) ^{2} \left( 2+b+d \right) ^{2}\geq 16\, \left( 1+a \right) \left( 1+b \right) \left( 1+c \right) \left( 1+d \right)(2+a+c)2(2+b+d)2≥16(1+a)(1+b)(1+c)(1+d)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_34495 (a b c d : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) : (2 + a + c) ^ 2 * (2 + b + d) ^ 2 ≥ 16 * (1 + a) * (1 + b) * (1 + c) * (1 + d) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph