lean_workbook_plus_14453

Proved

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

Let $m, n, x, y \in \mathbb{R^{+}}$ . If $x + y = m + n$ and $xy = mn$ , prove that $x = m$ or $x = n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14453 (x y m n : ℝ) (hx : 0 < x) (hy : 0 < y) (hm : 0 < m) (hn : 0 < n) (hxy : x + y = m + n) (hmn : x*y = m*n) : x = m ∨ x = n   :=  by sorry

Source

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

View graph