calc _ = 18 ^ 2 * 2 * α / 48 ^ 2 := by ring
  _ ≤ M := ?_
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 9 * α / 32 ≤ M
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α / 48 ^ 2 ≤ M