case h
R : Type ?u.598712
n : ℕ
⊢ ↑(μ * ↑ζ) n = ↑1 n
R : Type ?u.598712
⊢ μ * ↑ζ = 1
ext n
case h.refine'_1
R : Type ?u.598712
n : ℕ
⊢ ∀ (p n : ℕ), Prime p → 0 < n → ↑(μ * ↑ζ) (p ^ n) = ↑1 (p ^ n)

case h.refine'_2
R : Type ?u.598712
n : ℕ
⊢ ↑(μ * ↑ζ) 0 = ↑1 0

case h.refine'_3
R : Type ?u.598712
n : ℕ
⊢ ↑(μ * ↑ζ) 1 = ↑1 1

case h.refine'_4
R : Type ?u.598712
n : ℕ
⊢ ∀ (a b : ℕ), 1 < a → 1 < b → coprime a b → ↑(μ * ↑ζ) a = ↑1 a → ↑(μ * ↑ζ) b = ↑1 b → ↑(μ * ↑ζ) (a * b) = ↑1 (a * b)
case h
R : Type ?u.598712
n : ℕ
⊢ ↑(μ * ↑ζ) n = ↑1 n
refine' recOnPosPrimePosCoprime _ _ _ _ n
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ ↑(μ * ↑ζ) (p ^ n) = ↑1 (p ^ n)
case h.refine'_1
R : Type ?u.598712
n : ℕ
⊢ ∀ (p n : ℕ), Prime p → 0 < n → ↑(μ * ↑ζ) (p ^ n) = ↑1 (p ^ n)
intro p n hp hn
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ ∑ k in range n, ↑μ (p ^ (k + 1)) + ↑μ (p ^ 0) = ↑1 (p ^ n)
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ ↑(μ * ↑ζ) (p ^ n) = ↑1 (p ^ n)
rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ']
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ 0 = ↑1 (p ^ n)
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ ∑ k in range n, ↑μ (p ^ (k + 1)) + ↑μ (p ^ 0) = ↑1 (p ^ n)
simp_rw [Function.Embedding.coeFn_mk, pow_zero, moebius_apply_one,
  moebius_apply_prime_pow hp (Nat.succ_ne_zero _), Nat.succ_inj', sum_ite_eq', mem_range,
  if_pos hn, add_left_neg]
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ p ^ n ≠ 1
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ 0 = ↑1 (p ^ n)
rw [one_apply_ne]
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ ¬p = 1

case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ n ≠ 0
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ p ^ n ≠ 1
rw [Ne.def, pow_eq_one_iff]
no goals
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ ¬p = 1
exact hp.ne_one
no goals
case h.refine'_1
R : Type ?u.598712
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ n ≠ 0
exact hn.ne'
no goals
case h.refine'_2
R : Type ?u.598712
n : ℕ
⊢ ↑(μ * ↑ζ) 0 = ↑1 0
rw [ZeroHom.map_zero, ZeroHom.map_zero]
no goals
case h.refine'_3
R : Type ?u.598712
n : ℕ
⊢ ↑(μ * ↑ζ) 1 = ↑1 1
simp
case h.refine'_4
R : Type ?u.598712
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : coprime a b
ha' : ↑(μ * ↑ζ) a = ↑1 a
hb' : ↑(μ * ↑ζ) b = ↑1 b
⊢ ↑(μ * ↑ζ) (a * b) = ↑1 (a * b)
case h.refine'_4
R : Type ?u.598712
n : ℕ
⊢ ∀ (a b : ℕ), 1 < a → 1 < b → coprime a b → ↑(μ * ↑ζ) a = ↑1 a → ↑(μ * ↑ζ) b = ↑1 b → ↑(μ * ↑ζ) (a * b) = ↑1 (a * b)
intro a b _ha _hb hab ha' hb'
R : Type ?u.598712
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : coprime a b
ha' : ↑(μ * ↑ζ) a = ↑1 a
hb' : ↑(μ * ↑ζ) b = ↑1 b
⊢ IsMultiplicative (μ * ↑ζ)
case h.refine'_4
R : Type ?u.598712
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : coprime a b
ha' : ↑(μ * ↑ζ) a = ↑1 a
hb' : ↑(μ * ↑ζ) b = ↑1 b
⊢ ↑(μ * ↑ζ) (a * b) = ↑1 (a * b)
rw [IsMultiplicative.map_mul_of_coprime _ hab, ha', hb',
  IsMultiplicative.map_mul_of_coprime isMultiplicative_one hab]
no goals
R : Type ?u.598712
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : coprime a b
ha' : ↑(μ * ↑ζ) a = ↑1 a
hb' : ↑(μ * ↑ζ) b = ↑1 b
⊢ IsMultiplicative (μ * ↑ζ)
exact isMultiplicative_moebius.mul isMultiplicative_zeta.nat_cast