have h00 : u 0 = 1 := not_not.mp h0'
case intro.intro
u f : ℝ → ℝ
hm : StrictMono f ∨ StrictAnti f
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
h0' : u 0 ≠ 1 → False
⊢ ∃ 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
hy0 : ∀ (x : ℝ), f x = f x * u 0 + f 0
h0 : u 0 ≠ 1 → ∀ (x : ℝ), f x = f 0 / (1 - u 0)
h0' : u 0 ≠ 1 → False
h00 : u 0 = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp