calc 18 ^ 2 * 2 * α
    = 18 ^ 2 * α ^ 2 * α := by linear_combination -324 * α * hα
  _ = abs (-(18 ^ 2 * α ^ 2 * α)) := by rw [abs_neg, abs_of_nonneg]; positivity
  _ = |a * 2 * (a ^ 2 - 2 ^ 2) + 2 * c * (2 ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| := by ring_nf
  _ ≤ M * (a ^ 2 + 2 ^ 2 + c ^ 2) ^ 2 := by apply h
  _ = M * 48 ^ 2 := by linear_combination (324 * α ^ 2 + 1080) * M * hα
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 * α ≤ M * 48 ^ 2
no goals