lean_workbook_plus_35956

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_35956 (a b c : ℝ) : 3 * (a ^ 4 * b ^ 2 * c ^ 2 + b ^ 4 * c ^ 2 * a ^ 2 + c ^ 4 * a ^ 2 * b ^ 2) ≤ a ^ 4 * b ^ 4 + b ^ 4 * c ^ 4 + c ^ 4 * a ^ 4 + 2 * (a ^ 4 * b ^ 2 * c ^ 2 + b ^ 4 * c ^ 2 * a ^ 2 + c ^ 4 * a ^ 2 * b ^ 2)   :=  by sorry