have h0 : (u 0 ≠ 1) → ∀ x : ℝ, f x = f 0 / (1 - u 0) := by
  intro hu0 x
  have hy0x1 :=
              calc f 0 = f x - f x * u 0 := (sub_eq_of_eq_add' (hy0 x)).symm
              _ = f x * (1 - u 0) := by ring
  rw[hy0x1]
  have : 1 - u 0 ≠ 0 := sub_ne_zero.mpr hu0.symm
  field_simp
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
⊢ ∃ 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)
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp