lean_workbook_plus_46215

Proved

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

xy(x + y) = 30 \Rightarrow x + y = \frac{30}{xy} . Substitute into the second equation: xy + \frac{30}{xy} = 11 . Find xy: $x^2y^2 + 30 = 11xy \Rightarrow x^2y^2 - 11xy + 30 = 0 \Rightarrow (xy - 6)(xy - 5) = 0$ . So, xy = 6 or xy = 5 .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46215  (x y : ℝ)
  (h₀ : x * y * (x + y) = 30)
  (h₁ : x * y + (30 / (x * y)) = 11) :
  x + y = (30 / (x * y))   :=  by sorry

Source

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

View graph