Lean-Workbook Plus 66159: A weighted cyclic real-power identity

For all real $a,b,c,r$, $(a^r+b^r-c^r)(a-b)^2+(b^r+c^r-a^r)(b-c)^2+(c^r+a^r-b^r)(c-a)^2=2\bigl(a^r(a-b)(a-c)+b^r(b-c)(b-a)+c^r(c-a)(c-b)\bigr)$. Powers use Lean's total real-power convention.

Source: Lean-Workbook row lean_workbook_plus_66159 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.