have h2 : ∀ x, (u x) * u (-x) = 1 := by
  intro x
  have := hu x (-x)
  rw [add_right_neg] at this
  rw [←this]
  exact hu0
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
⊢ ∃ k, ∀ (x : ℝ), u x = (k * x).exp