Prove2Me

lean_workbook_plus_3707

Proved

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

The second equation can be rewritten as x2+y2xy=2512\frac{x^2+y^2}{xy}=\frac{25}{12} . Squaring the first equation we find that x2+2xy+y2=49  ⟹  x2+y2=49−2xyx^2+2xy+y^2=49 \implies x^2+y^2=49-2xy . Substituting into our second equation, we have\n\n49−2xyxy=2512\frac{49-2xy}{xy}=\frac{25}{12}\n\n  ⟹  49xy−2=2512\implies \frac{49}{xy}-2=\frac{25}{12}\n\n  ⟹  49xy=4912  ⟹  xy=12\implies \frac{49}{xy}=\frac{49}{12} \implies xy=12 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3707  (x y : ℝ)
  (h₀ : 0 < x ∧ 0 < y)
  (h₁ : x + y = 7)
  (h₂ : (x^2 + y^2) / (x * y) = 25 / 12) :
  x * y = 12   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph