let f : ℝ → ℝ := λ x ↦ Real.exp (k * x) - 1
case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
case intro.inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
⊢ ∃ f, (StrictMono f ∨ StrictAnti f) ∧ ∀ (x y : ℝ), f (x + y) = f x * u y + f y