swap
case inr
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2

s x y z : ℝ
hxyz : x + y + z = 0
h' : 0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
s x y z : ℝ
hxyz : x + y + z = 0
h' : 0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2

case inr
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2