A four-variable quartic sum bounds mixed products

(a+b)(ac^{2}+bd^{2})=a^{2}c^{2}+b^{2}d^{2}+abd^{2}+abc^{2} by AM-GM inequality,we can prove this inequality: $2(a^{4}+b^{4}+c^{4}+d^{4})\geq 2(a^{2}c^{2}+b^{2}d^{2}+abd^{2}+abc^{2})$

Source: InternLM Lean-Workbook, record lean_workbook_31356 (Apache-2.0). Complete source proposition preserved; proof developed independently.