lean_workbook_plus_8211

Proved

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

Find the value of $x^2 - y^2$ given $x - y = 7$ and $x \cdot y = 8$ (Edit: with corrected solution).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8211 (x y : ℝ) (h₁ : x - y = 7) (h₂ : x * y = 8) : x^2 - y^2 = 63 ∨ x^2 - y^2 = -63   :=  by sorry

Source