intro n
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
⊢ ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
n : ℕ
⊢ ∀ (x : ℝ), u (↑n * x) = u x ^ n