lean_workbook_plus_17703

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Denote t=xy. Now $a^3=(x+y)^3=x^3+y^3+3xy(x+y)=x^3+y^3+3at\implies x^3+y^3=a^3-3at$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17703  (x y a t : ℝ)
  (h₀ : t = x * y)
  (h₁ : a = x + y) :
  x^3 + y^3 = a^3 - 3 * a * t   :=  by sorry

Source