lean_workbook_plus_72719

Proved

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

Find the value of $x$ so that the function $q(x)=\frac{1}{2}x-3$ has the given value $q(x)=-4$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72719 (x : ℝ) (q : ℝ → ℝ) (h₁ : q = fun (x : ℝ) => 1 / 2 * x - 3) : q x = -4 ↔ x = -2   :=  by sorry

Source