case ofNat
x✝ y x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.ofNat a✝) = ↑(Int.ofNat a✝) * log x

case negSucc
x✝ y x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.negSucc a✝) = ↑(Int.negSucc a✝) * log x
x✝ y x : ℝ
n : ℤ
⊢ log (x ^ n) = ↑n * log x
induction n
no goals
case negSucc
x✝ y x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.negSucc a✝) = ↑(Int.negSucc a✝) * log x
rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]
no goals
case ofNat
x✝ y x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.ofNat a✝) = ↑(Int.ofNat a✝) * log x
rw [Int.ofNat_eq_coe, zpow_ofNat, log_pow, Int.cast_ofNat]