case zero
x✝ y x : ℝ
⊢ log (x ^ Nat.zero) = ↑Nat.zero * log x

case succ
x✝ y x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
⊢ log (x ^ Nat.succ n) = ↑(Nat.succ n) * log x
x✝ y x : ℝ
n : ℕ
⊢ log (x ^ n) = ↑n * log x
induction' n with n ih
case succ.inl
x y : ℝ
n : ℕ
ih : log (0 ^ n) = ↑n * log 0
⊢ log (0 ^ Nat.succ n) = ↑(Nat.succ n) * log 0

case succ.inr
x✝ y x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ Nat.succ n) = ↑(Nat.succ n) * log x
case succ
x✝ y x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
⊢ log (x ^ Nat.succ n) = ↑(Nat.succ n) * log x
rcases eq_or_ne x 0 with (rfl | hx)
no goals
case succ.inr
x✝ y x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ Nat.succ n) = ↑(Nat.succ n) * log x
rw [pow_succ', log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]
no goals
case zero
x✝ y x : ℝ
⊢ log (x ^ Nat.zero) = ↑Nat.zero * log x
simp
no goals
case succ.inl
x y : ℝ
n : ℕ
ih : log (0 ^ n) = ↑n * log 0
⊢ log (0 ^ Nat.succ n) = ↑(Nat.succ n) * log 0
simp