case h
R : Type ?u.525734
k x✝ : ℕ
⊢ ↑(ζ * pow k) x✝ = ↑(σ k) x✝
R : Type ?u.525734
k : ℕ
⊢ ζ * pow k = σ k
ext
case h
R : Type ?u.525734
k x✝ : ℕ
⊢ ∑ i in divisors x✝, ↑(pow k) i =
    ↑{ toFun := fun n => ∑ d in divisors n, d ^ k, map_zero' := (_ : ∑ d in divisors 0, d ^ k = 0) } x✝
case h
R : Type ?u.525734
k x✝ : ℕ
⊢ ↑(ζ * pow k) x✝ = ↑(σ k) x✝
rw [sigma, zeta_mul_apply]
case h
R : Type ?u.525734
k x✝ : ℕ
⊢ ∀ (x : ℕ), x ∈ divisors x✝ → ↑(pow k) x = x ^ k
case h
R : Type ?u.525734
k x✝ : ℕ
⊢ ∑ i in divisors x✝, ↑(pow k) i =
    ↑{ toFun := fun n => ∑ d in divisors n, d ^ k, map_zero' := (_ : ∑ d in divisors 0, d ^ k = 0) } x✝
apply sum_congr rfl
case h
R : Type ?u.525734
k x✝ x : ℕ
hx : x ∈ divisors x✝
⊢ ↑(pow k) x = x ^ k
case h
R : Type ?u.525734
k x✝ : ℕ
⊢ ∀ (x : ℕ), x ∈ divisors x✝ → ↑(pow k) x = x ^ k
intro x hx
R : Type ?u.525734
k x✝ x : ℕ
hx : x ∈ divisors x✝
⊢ ¬x = 0
case h
R : Type ?u.525734
k x✝ x : ℕ
hx : x ∈ divisors x✝
⊢ ↑(pow k) x = x ^ k
rw [pow_apply, if_neg (not_and_of_not_right _ _)]
R : Type ?u.525734
k x✝ x : ℕ
hx : x = 0
⊢ ¬x ∈ divisors x✝
R : Type ?u.525734
k x✝ x : ℕ
hx : x ∈ divisors x✝
⊢ ¬x = 0
contrapose! hx
no goals
R : Type ?u.525734
k x✝ x : ℕ
hx : x = 0
⊢ ¬x ∈ divisors x✝
simp [hx]