Inverse function theorem (statement)

import Mathlib

theorem inverse_function_thm {f : ℝ → ℝ} {a : ℝ} (hf : ContDiffAt ℝ 1 f a) (hf' : deriv f a ≠ 0) : ∃ g : ℝ → ℝ, ∃ U ∈ nhds a, ∀ x ∈ U, g (f x) = x ∧ f (g x) = x :=sorry