-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_mul_coe_zeta : (μ * ζ : ArithmeticFunction ℤ) = 1

Proof state:
⊢ μ * ↑ζ = 1

Tactic:
ext n

Result:
case h
n : ℕ
⊢ (μ * ↑ζ) n = 1 n

Proof state:
case h.refine_1
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → 0 < n → (μ * ↑ζ) (p ^ n) = 1 (p ^ n)

Tactic:
intro p n hp hn

Result:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ (μ * ↑ζ) (p ^ n) = 1 (p ^ n)

Proof state:
case h
n : ℕ
⊢ (μ * ↑ζ) n = 1 n

Tactic:
refine recOnPosPrimePosCoprime ?_ ?_ ?_ ?_ n

Result:
case h.refine_1
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → 0 < n → (μ * ↑ζ) (p ^ n) = 1 (p ^ n)

case h.refine_2
n : ℕ
⊢ (μ * ↑ζ) 0 = 1 0

case h.refine_3
n : ℕ
⊢ (μ * ↑ζ) 1 = 1 1

case h.refine_4
n : ℕ
⊢ ∀ (a b : ℕ), 1 < a → 1 < b → a.Coprime b → (μ * ↑ζ) a = 1 a → (μ * ↑ζ) b = 1 b → (μ * ↑ζ) (a * b) = 1 (a * b)

Proof state:
case h.refine_4
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ (μ * ↑ζ) (a * b) = 1 (a * b)

Tactic:
rw [IsMultiplicative.map_mul_of_coprime _ hab, ha', hb',
  IsMultiplicative.map_mul_of_coprime isMultiplicative_one hab]

Result:
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ (μ * ↑ζ).IsMultiplicative

Proof state:
case h.refine_2
n : ℕ
⊢ (μ * ↑ζ) 0 = 1 0

Tactic:
rw [ZeroHom.map_zero, ZeroHom.map_zero]

Result:
no goals

Proof state:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ p ^ n ≠ 1

Tactic:
rw [Ne, pow_eq_one_iff]

Result:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ ¬p = 1

case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ n ≠ 0

Proof state:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ ∑ k ∈ range n, μ (p ^ (k + 1)) + μ (p ^ 0) = 1 (p ^ n)

Tactic:
simp_rw [Nat.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, neg_add_cancel]

Result:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ 0 = 1 (p ^ n)

Proof state:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ 0 = 1 (p ^ n)

Tactic:
rw [one_apply_ne]

Result:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ p ^ n ≠ 1

Proof state:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ ¬p = 1

Tactic:
exact hp.ne_one

Result:
no goals

Proof state:
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ (μ * ↑ζ).IsMultiplicative

Tactic:
exact isMultiplicative_moebius.mul isMultiplicative_zeta.natCast

Result:
no goals

Proof state:
case h.refine_4
n : ℕ
⊢ ∀ (a b : ℕ), 1 < a → 1 < b → a.Coprime b → (μ * ↑ζ) a = 1 a → (μ * ↑ζ) b = 1 b → (μ * ↑ζ) (a * b) = 1 (a * b)

Tactic:
intro a b _ha _hb hab ha' hb'

Result:
case h.refine_4
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ (μ * ↑ζ) (a * b) = 1 (a * b)

Proof state:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ n ≠ 0

Tactic:
exact hn.ne'

Result:
no goals

Proof state:
case h.refine_3
n : ℕ
⊢ (μ * ↑ζ) 1 = 1 1

Tactic:
simp

Result:
no goals

Proof state:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ (μ * ↑ζ) (p ^ n) = 1 (p ^ n)

Tactic:
rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ']

Result:
case h.refine_1
n✝ p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ ∑ k ∈ range n, μ (p ^ (k + 1)) + μ (p ^ 0) = 1 (p ^ n)