A fifth-power identity under a linear constraint
ProvedWorkbookSource.problem_20723lean-workbooksource-checked
If $x+y+1=0$ then $2(x^5+y^5+1)=5xy(x^2+y^2+1)$
Source: InternLM Lean-Workbook, record lean_workbook_20723 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_20723 (x y : ℝ) (h : x + y + 1 = 0) : 2 * (x^5 + y^5 + 1) = 5 * x * y * (x^2 + y^2 + 1) := by sorry
Source