lean_workbook_plus_36582

Proved

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

Given $a+\frac{b^2}{a}=b+\frac{a^2}{b}$ , prove that $a=b$ for nonzero real numbers $a$ and $b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36582 (a b : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (hab : a + b^2 / a = b + a^2 / b) : a = b   :=  by sorry

Source