lean_workbook_plus_28189

Proved

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

If $g(x)=\begin{cases}3x+21&x\ne 0\\21&x=0\end{cases}$ , what's the answer and reasoning?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28189 (g : ℝ → ℝ) (g_of : ∀ x, x ≠ 0 → g x = 3 * x + 21) (g_on : g 0 = 21) : ∀ x, g x = 3 * x + 21   :=  by sorry

Source