lean_workbook_plus_33945

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_33945 (f : ℝ → ℝ) (x : ℝ) (f_of_le : x ≤ -1 / 2 → f x = x - 2) (f_of_ge : -1 / 2 ≤ x → f x = 5 * x) : f x = if x ≤ -1 / 2 then x - 2 else 5 * x   :=  by sorry