case inl
x y : ℝ
⊢ log ↑0 = Finsupp.sum (Nat.factorization 0) fun p t => ↑t * log ↑p

case inr
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => ↑t * log ↑p
x y : ℝ
n : ℕ
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => ↑t * log ↑p
rcases eq_or_ne n 0 with (rfl | hn)
no goals
case inl
x y : ℝ
⊢ log ↑0 = Finsupp.sum (Nat.factorization 0) fun p t => ↑t * log ↑p
simp
case inr
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => log ↑(p ^ t)
case inr
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => ↑t * log ↑p
simp only [← log_pow, ← Nat.cast_pow]
case inr.hg
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ ↑(Nat.factorization n) a) = 0 → ↑(Nat.factorization n) a = 0
case inr
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ log ↑n = Finsupp.sum (Nat.factorization n) fun p t => log ↑(p ^ t)
rw [← Finsupp.log_prod, ← Nat.cast_finsupp_prod, Nat.factorization_prod_pow_eq_self hn]
case inr.hg
x y : ℝ
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ ↑(Nat.factorization n) p) = 0
⊢ ↑(Nat.factorization n) p = 0
case inr.hg
x y : ℝ
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ ↑(Nat.factorization n) a) = 0 → ↑(Nat.factorization n) a = 0
intro p hp
no goals
case inr.hg
x y : ℝ
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ ↑(Nat.factorization n) p) = 0
⊢ ↑(Nat.factorization n) p = 0
rw [pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]