Quartic polynomial strict midpoint convexity gap

import Mathlib

theorem quartic_convexity_gap_scalar (x z : ℝ) : ((x + z) / 2) ^ 4 + (x - z) ^ 2 * (7 * x ^ 2 + 10 * x * z + 7 * z ^ 2) / 16 = (1 / 2 : ℝ) * x ^ 4 + (1 / 2 : ℝ) * z ^ 4 := by sorry