lean_workbook_plus_49683

Proved

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

Let $f(x) = \dfrac{2x + 5}{x + 2} = 2 + \dfrac{1}{x + 2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49683 (x : ℝ) (hx : x ≠ -2) : (2 * x + 5) / (x + 2) = 2 + 1 / (x + 2)   :=  by sorry

Source