have h3 : ∀ x y : ℝ, x ≠ 0 → y ≠ 0 → (u x - 1) / f x =  (u y - 1) / f y := by
  intro x y hx hy
  have hx1 := hfx0 x hx
  have hy1 := hfx0 y hy
  have := h2 x y
  field_simp
  linarith
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 * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
⊢ ∃ 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 * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
hfx0 : ∀ (x : ℝ), x ≠ 0 → f x ≠ 0
h1 : ∀ (x y : ℝ), f x * u y + f y = f x + f y * u x
h2 : ∀ (x y : ℝ), f x * (u y - 1) = f y * (u x - 1)
h3 : ∀ (x y : ℝ), x ≠ 0 → y ≠ 0 → (u x - 1) / f x = (u y - 1) / f y
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp