lean_workbook_plus_60816

Open

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

Let $f(x) = \left(e^{x} + 1\right)\left(e^{x} + x + 1\right) = e^{2x} + (x + 2)e^{x} + x + 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60816 (x : ℝ) : (exp x + 1) * (exp x + x + 1) = exp (2 * x) + (x + 2) * exp x + x + 1   :=  by sorry

Source