lean_workbook_plus_4332

Proved

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

we have $x+y=7$ and $x^2 -y^2=21$ \n\nFactoring $x^2 -y^2=21$ to get $(x-y)(x+y)=21$ \n\nFrom there $x-y=3$ . Now adding $x+y=7$ to $x-y=3$ yields $x=5$ , $y=2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4332  (x y : ℝ)
  (h₀ : x + y = 7)
  (h₁ : x^2 - y^2 = 21) :
  x = 5 ∧ y = 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph