lean_workbook_plus_57173

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_57173 : ∀ a b c d : ℝ, a^2 + b^2 + c^2 + d^2 + a * b * c * d + 1 ≥ a * b + a * c + a * d + b * c + b * d + c * d   :=  by sorry