rw[hp1, hu (↑pn * x) x, hpn x, mul_comm]
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
hp1 : ↑pn.succ * x = ↑pn * x + x
⊢ u (↑(pn + 1) * x) = u x ^ (pn + 1)
case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
hp1 : ↑pn.succ * x = ↑pn * x + x
⊢ u x * u x ^ pn = u x ^ (pn + 1)