simp only [Nat.zero_eq, CharP.cast_eq_zero, zero_mul, Real.rpow_zero]
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
x : ℝ
⊢ u (↑0 * x) = u x ^ 0
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
x : ℝ
⊢ u 0 = u x ^ 0