obtain ⟨f, hm, hf⟩ := h
u : ℝ → ℝ
h : ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp