Prove2Me

lean_workbook_plus_18359

Proved

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

Find f(g(h(x)))f(g(h(x))) where f(x)=2x−3f(x) = 2x - 3, g(x)=12x2−xg(x) = \frac{1}{2}x^2 - x, and h(x)=x2+2h(x) = x^2 + 2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18359 (f g h : ℝ → ℝ) (f_def : ∀ x, f x = 2 * x - 3) (g_def : ∀ x, g x = 1 / 2 * x^2 - x) (h_def : ∀ x, h x = x^2 + 2) : ∀ x, f (g (h x)) = x^4 + 2 * x^2 - 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph