lean_workbook_plus_25699Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)prove that: \n\n (a+b)(b+c)(c+d)(d+a)≥(a+b+c+d)(acd+abd+abc+bcd)\left( a+b \right) \left( b+c \right) \left( c+d \right) \left( d+ a \right) \geq \left( a+b+c+d \right) \left( acd+abd+abc+bcd \right) (a+b)(b+c)(c+d)(d+a)≥(a+b+c+d)(acd+abd+abc+bcd)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_25699 (a b c d : ℝ) : (a + b) * (b + c) * (c + d) * (d + a) ≥ (a + b + c + d) * (a * c * d + a * b * d + a * b * c + b * c * d) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph