have this :=
  calc
    2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2)
      ≤ _ * _ ^ 3 := by gcongr; exact lhs_ineq hxy
    _ ≤ (3 * (x + y) ^ 2 + 2 * s ^ 2) ^ 4 / 4 ^ 4 := mid_ineq
    _ ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4 := by
        gcongr (?_ + _) ^ 4 / _
        apply rhs_ineq
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2