lean_workbook_plus_14445

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_14445 : ∀ a b c d : ℝ, a * b ^ 4 * c + b * c ^ 4 * d + a * c * d ^ 4 + a ^ 4 * b * d ≥ a * b * c * d * (a ^ 2 + c ^ 2 + b ^ 2 + d ^ 2)   :=  by sorry