awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p : ℕ
hp : Nat.Prime p
rw : HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) p : ℕ) = -1
rw₁ : HPow.hPow (α := ℤ) (β := ℕ) (-1) 1 = -1
rw₂ rw₃ : Eq (α := ℤ) (-1) (-1)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) p : ℤ) (-1 : ℤ)

Tactic:
rw [moebius_apply_of_squarefree hp.squarefree, cardFactors_apply_prime hp, pow_one]

Premises used: ArithmeticFunction.moebius_apply_of_squarefree, Irreducible.squarefree, pow_one, ArithmeticFunction.cardFactors_apply_prime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
pos : ∀ (h : k = 1), Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (-1 : ℤ)
neg : ∀ (h : ¬k = 1), Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (if k = 1 then -1 else 0 : ℤ)

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
pos : Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (HPow.hPow (β := ℕ) p 1) : ℤ) (-1 : ℤ)
pos₁ : Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) p : ℤ) (-1 : ℤ)
pos₂ pos₃ : Eq (α := ℤ) (-1) (-1)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (-1 : ℤ)

Tactic:
rw [h, pow_one, moebius_apply_prime hp]

Premises used: ArithmeticFunction.moebius_apply_prime, pow_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
neg : ¬Squarefree (p ^ k)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (0 : ℤ)

Tactic:
rw [moebius_eq_zero_of_not_squarefree]

Premises used: ArithmeticFunction.moebius_eq_zero_of_not_squarefree
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
neg : ¬Squarefree p ∨ ¬k = 1
⊢ ¬Squarefree (p ^ k)

Tactic:
rw [squarefree_pow_iff hp.ne_one hk, not_and_or]

Premises used: Nat.squarefree_pow_iff, Nat.Prime.ne_one, not_and_or
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree p ∨ ¬k = 1

Tactic:
Or.inr h

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree p ∨ ¬k = 1

Tactic:
exact Or.inr h

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
hn : IsPrimePow n
hn' : ¬Nat.Prime n
obtain :
  ∀ (p k : ℕ) (hp : Nat.Prime p) (hk : 0 < k) (hn : IsPrimePow (p ^ k)) (hn' : ¬Nat.Prime (p ^ k)),
    Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)

Tactic:
obtain ⟨p, k, hp, hk, rfl⟩ := (isPrimePow_nat_iff _).1 hn

Premises used: isPrimePow_nat_iff, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
hnc : ¬k = 1
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (0 : ℤ)

Tactic:
rw [moebius_apply_prime_pow hp hk.ne', if_neg]

Premises used: ArithmeticFunction.moebius_apply_prime_pow, LT.lt.ne', if_neg
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p : ℕ
hp : Nat.Prime p
hk : LT.lt (α := ℕ) 0 1
hn : IsPrimePow (HPow.hPow (β := ℕ) p 1)
hn' : ¬Nat.Prime (HPow.hPow (β := ℕ) p 1)
⊢ Nat.Prime (HPow.hPow (β := ℕ) p 1)

Tactic:
simpa
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p : ℕ
hp : Nat.Prime p
hk : LT.lt (α := ℕ) 0 1
hn : IsPrimePow (HPow.hPow (β := ℕ) p 1)
hn' : ¬Nat.Prime (HPow.hPow (β := ℕ) p 1)
⊢ False

Tactic:
exact hn' (by simpa)
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
rw :
  Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) 1 : ℤ) (1 : ℤ) ∧
    ∀ {m n : ℕ},
      m ≠ 0 →
        n ≠ 0 →
          m.Coprime n →
            (μ : (a : ℕ) → ℤ) (m * n) = HMul.hMul (α := ℤ) (β := ℤ) ((μ : (a : ℕ) → ℤ) m : ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ)
⊢ μ.IsMultiplicative

Tactic:
rw [IsMultiplicative.iff_ne_zero]

Premises used: ArithmeticFunction.IsMultiplicative.iff_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
refine :
  ∀ {n m : ℕ} (hn : n ≠ 0) (hm : m ≠ 0) (hnm : n.Coprime m),
    (μ : (a : ℕ) → ℤ) (n * m) = HMul.hMul (α := ℤ) (β := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) ((μ : (a : ℕ) → ℤ) m : ℤ)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) 1 : ℤ) (1 : ℤ) ∧
    ∀ {m n : ℕ},
      m ≠ 0 →
        n ≠ 0 →
          m.Coprime n →
            (μ : (a : ℕ) → ℤ) (m * n) = HMul.hMul (α := ℤ) (β := ℤ) ((μ : (a : ℕ) → ℤ) m : ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ)

Tactic:
refine ⟨by simp, fun {n m} hn hm hnm => ?_⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : n.Coprime m
⊢ (μ : (a : ℕ) → ℤ) (n * m) = HMul.hMul (α := ℤ) (β := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) ((μ : (a : ℕ) → ℤ) m : ℤ)

Tactic:
simp only [moebius, coe_mk, squarefree_mul hnm, ite_zero_mul_ite_zero, cardFactors_mul hn hm,
    pow_add]

Premises used: ite_zero_mul_ite_zero, pow_add, ArithmeticFunction.coe_mk, ArithmeticFunction.moebius, ArithmeticFunction.cardFactors_mul, Nat.squarefree_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
h_mult : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
trans :
  Eq.{u_1 + 1} (α := R) (∏ p ∈ n.primeFactors, HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) : R)
    ((ArithmeticFunction.prodPrimeFactors fun (p : ℕ) ↦
            (HAdd.hAdd (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) p :
          (a : ℕ) → R)
        n :
      R)
trans₁ :
  Eq.{u_1 + 1} (α := R)
    ((ArithmeticFunction.prodPrimeFactors fun (p : ℕ) ↦
            (HAdd.hAdd (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) p :
          (a : ℕ) → R)
        n :
      R)
    (∑ d ∈ n.divisors, (f : (a : ℕ) → R) d : R)
⊢ Eq.{u_1 + 1} (α := R) (∏ p ∈ n.primeFactors, HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R))
    (∑ d ∈ n.divisors, (f : (a : ℕ) → R) d)

Tactic:
trans (∏ᵖ p ∣ n, ((ζ : ArithmeticFunction R) + f) p)

Premises used: ArithmeticFunction.zeta, ArithmeticFunction.natToArithmeticFunction, ArithmeticFunction.prodPrimeFactors, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
h_mult : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
simp_rw :
  Eq.{u_1 + 1} (α := R) (∏ p ∈ n.primeFactors, HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R))
    (∏ x ∈ n.primeFactors, HAdd.hAdd (α := R) (β := R) ((↑((ζ : (a : ℕ) → ℕ) x) : R) : R) ((f : (a : ℕ) → R) x : R))
⊢ Eq.{u_1 + 1} (α := R) (∏ p ∈ n.primeFactors, HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) : R)
    ((ArithmeticFunction.prodPrimeFactors fun (p : ℕ) ↦
            (HAdd.hAdd (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) p :
          (a : ℕ) → R)
        n :
      R)

Tactic:
simp_rw [prodPrimeFactors_apply hn.ne_zero, add_apply, natCoe_apply]

Premises used: ArithmeticFunction.add_apply, ArithmeticFunction.prodPrimeFactors_apply, Squarefree.ne_zero, ArithmeticFunction.natCoe_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
h_mult : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
apply :
  ∀ x ∈ n.primeFactors,
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) x : R) =
      HAdd.hAdd (α := R) (β := R) ((↑((ζ : (a : ℕ) → ℕ) x) : R) : R) ((f : (a : ℕ) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) (∏ p ∈ n.primeFactors, HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R))
    (∏ x ∈ n.primeFactors, HAdd.hAdd (α := R) (β := R) ((↑((ζ : (a : ℕ) → ℕ) x) : R) : R) ((f : (a : ℕ) → R) x : R))

Tactic:
apply prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
h_mult : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
rw :
  HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
    HAdd.hAdd (α := R) (β := R) ((↑1 : R) : R) ((f : (a : ℕ) → R) p : R)
rw₁ rw₂ :
  HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R)
⊢ HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
    HAdd.hAdd (α := R) (β := R) ((↑((ζ : (a : ℕ) → ℕ) p) : R) : R) ((f : (a : ℕ) → R) p : R)

Tactic:
rw [zeta_apply_ne (prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp).ne_zero, cast_one]

Premises used: List.mem_toFinset, Nat.prime_of_mem_primeFactorsList, ArithmeticFunction.zeta_apply_ne, Nat.Prime.ne_zero, Iff.mp, Nat.cast_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
h_mult : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
rw :
  Eq (α := R)
    ((HMul.hMul (α := ArithmeticFunction R) ((↑ζ : ArithmeticFunction R) : ArithmeticFunction R) f : (a : ℕ) → R) n : R)
    (∑ d ∈ n.divisors, (f : (a : ℕ) → R) d : R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ n.divisors, (f : (a : ℕ) → R) i) (∑ d ∈ n.divisors, (f : (a : ℕ) → R) d)
⊢ Eq.{u_1 + 1} (α := R)
    ((ArithmeticFunction.prodPrimeFactors fun (p : ℕ) ↦
            (HAdd.hAdd (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) p :
          (a : ℕ) → R)
        n :
      R)
    (∑ d ∈ n.divisors, (f : (a : ℕ) → R) d : R)

Tactic:
rw [isMultiplicative_zeta.natCast.prodPrimeFactors_add_of_squarefree h_mult hn,
    coe_zeta_mul_apply]

Premises used: ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree, ArithmeticFunction.IsMultiplicative.natCast, ArithmeticFunction.isMultiplicative_zeta, ArithmeticFunction.coe_zeta_mul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
trans :
  Eq.{u_1 + 1} (α := R) (∏ p ∈ n.primeFactors, HSub.hSub (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R))
    (∏ p ∈ n.primeFactors,
      HAdd.hAdd (α := R) (β := R) (1 : R) ((ArithmeticFunction.pmul (↑μ : ArithmeticFunction R) f : (a : ℕ) → R) p : R))
trans₁ :
  Eq.{u_1 + 1} (α := R)
    (∏ p ∈ n.primeFactors,
      HAdd.hAdd (α := R) (β := R) (1 : R) ((ArithmeticFunction.pmul (↑μ : ArithmeticFunction R) f : (a : ℕ) → R) p : R))
    (∑ d ∈ n.divisors, HMul.hMul (α := R) (β := R) ((↑((μ : (a : ℕ) → ℤ) d) : R) : R) ((f : (a : ℕ) → R) d : R))
⊢ Eq.{u_1 + 1} (α := R) (∏ p ∈ n.primeFactors, HSub.hSub (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R))
    (∑ d ∈ n.divisors, HMul.hMul (α := R) (β := R) ((↑((μ : (a : ℕ) → ℤ) d) : R) : R) ((f : (a : ℕ) → R) d : R))

Tactic:
trans (∏ p ∈ n.primeFactors, (1 + (ArithmeticFunction.pmul (μ : ArithmeticFunction R) f) p))

Premises used: ArithmeticFunction.pmul, ArithmeticFunction.ofInt, Finset.prod, HAdd.hAdd, ArithmeticFunction.moebius, Nat.primeFactors, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
apply :
  ∀ x ∈ n.primeFactors,
    HSub.hSub (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) x : R) =
      HAdd.hAdd (α := R) (β := R) (1 : R) ((ArithmeticFunction.pmul (↑μ : ArithmeticFunction R) f : (a : ℕ) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) (∏ p ∈ n.primeFactors, HSub.hSub (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R))
    (∏ p ∈ n.primeFactors,
      HAdd.hAdd (α := R) (β := R) (1 : R) ((ArithmeticFunction.pmul (↑μ : ArithmeticFunction R) f : (a : ℕ) → R) p : R))

Tactic:
apply prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
rw :
  HSub.hSub (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
    1 + HMul.hMul (α := R) (β := R) ((↑(-1) : R) : R) ((f : (a : ℕ) → R) p : R)
⊢ HSub.hSub (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((ArithmeticFunction.pmul (↑μ : ArithmeticFunction R) f : (a : ℕ) → R) p : R)

Tactic:
rw [pmul_apply, intCoe_apply, ArithmeticFunction.moebius_apply_prime
        (prime_of_mem_primeFactorsList (List.mem_toFinset.mp hp))]

Premises used: List.mem_toFinset, Nat.prime_of_mem_primeFactorsList, ArithmeticFunction.pmul_apply, ArithmeticFunction.moebius_apply_prime, Iff.mp, ArithmeticFunction.intCoe_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ HSub.hSub (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
    1 + HMul.hMul (α := R) (β := R) ((↑(-1) : R) : R) ((f : (a : ℕ) → R) p : R)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
rw :
  Eq.{u_1 + 1} (α := R) (∑ d ∈ n.divisors, (ArithmeticFunction.pmul (↑μ : ArithmeticFunction R) f : (a : ℕ) → R) d)
    (∑ d ∈ n.divisors, HMul.hMul (α := R) (β := R) ((↑((μ : (a : ℕ) → ℤ) d) : R) : R) ((f : (a : ℕ) → R) d : R))
⊢ Eq.{u_1 + 1} (α := R)
    (∏ p ∈ n.primeFactors,
      HAdd.hAdd (α := R) (β := R) (1 : R) ((ArithmeticFunction.pmul (↑μ : ArithmeticFunction R) f : (a : ℕ) → R) p : R))
    (∑ d ∈ n.divisors, HMul.hMul (α := R) (β := R) ((↑((μ : (a : ℕ) → ℤ) d) : R) : R) ((f : (a : ℕ) → R) d : R))

Tactic:
rw [(isMultiplicative_moebius.intCast.pmul hf).prodPrimeFactors_one_add_of_squarefree hn]

Premises used: ArithmeticFunction.IsMultiplicative.pmul, ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
simp_rw :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ n.divisors,
      HMul.hMul (α := R) (β := R) ((((↑μ : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) x : R)
        ((f : (a : ℕ) → R) x : R))
    (∑ d ∈ n.divisors, HMul.hMul (α := R) (β := R) ((↑((μ : (a : ℕ) → ℤ) d) : R) : R) ((f : (a : ℕ) → R) d : R))
⊢ Eq.{u_1 + 1} (α := R) (∑ d ∈ n.divisors, (ArithmeticFunction.pmul (↑μ : ArithmeticFunction R) f : (a : ℕ) → R) d)
    (∑ d ∈ n.divisors, HMul.hMul (α := R) (β := R) ((↑((μ : (a : ℕ) → ℤ) d) : R) : R) ((f : (a : ℕ) → R) d : R))

Tactic:
simp_rw [pmul_apply, intCoe_apply]

Premises used: ArithmeticFunction.pmul_apply, ArithmeticFunction.intCoe_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
h : ∀ (n : ℕ), Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) n : ℤ) ((1 : (a : ℕ) → ℤ) n : ℤ)
⊢ μ * (↑ζ : ArithmeticFunction ℤ) = 1

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
h : Eq (α := ℤ) (0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)
h₁ h₂ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)

Tactic:
rw [map_zero, map_zero]

Premises used: ArithmeticFunction.map_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 1 : ℤ) ((1 : (a : ℕ) → ℤ) 1 : ℤ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p n : ℕ
hp : Nat.Prime p
hn : 0 < n
h :
  HAdd.hAdd (α := ℤ) (β := ℤ) (∑ k ∈ range n, (μ : (a : ℕ) → ℤ) (p ^ (k + 1)) : ℤ)
      ((μ : (a : ℕ) → ℤ) (HPow.hPow (β := ℕ) p 0) : ℤ) =
    (1 : (a : ℕ) → ℤ) (p ^ n)
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) (p ^ n) : ℤ) ((1 : (a : ℕ) → ℤ) (p ^ n) : ℤ)

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

Premises used: Nat.sum_divisors_prime_pow, ArithmeticFunction.coe_mul_zeta_apply, Finset.sum_range_succ'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ HAdd.hAdd (α := ℤ) (β := ℤ) (∑ k ∈ range n, (μ : (a : ℕ) → ℤ) (p ^ (k + 1)) : ℤ)
      ((μ : (a : ℕ) → ℤ) (HPow.hPow (β := ℕ) p 0) : ℤ) =
    (1 : (a : ℕ) → ℤ) (p ^ n)

Tactic:
simp [moebius_apply_prime_pow, hp.ne_one, hn.ne', hp, hn]

Premises used: ArithmeticFunction.moebius_apply_prime_pow, LT.lt.ne', Nat.Prime.ne_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) a : ℤ) ((1 : (a : ℕ) → ℤ) a : ℤ)
hb' : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) b : ℤ) ((1 : (a : ℕ) → ℤ) b : ℤ)
rw : (μ * (↑ζ : ArithmeticFunction ℤ)).IsMultiplicative
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) (a * b) : ℤ) ((1 : (a : ℕ) → ℤ) (a * b) : ℤ)

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

Premises used: ArithmeticFunction.isMultiplicative_one, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) a : ℤ) ((1 : (a : ℕ) → ℤ) a : ℤ)
hb' : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) b : ℤ) ((1 : (a : ℕ) → ℤ) b : ℤ)
⊢ (μ * (↑ζ : ArithmeticFunction ℤ)).IsMultiplicative

Tactic:
isMultiplicative_moebius.mul isMultiplicative_zeta.natCast

Premises used: ArithmeticFunction.IsMultiplicative.natCast, ArithmeticFunction.isMultiplicative_zeta, ArithmeticFunction.isMultiplicative_moebius, ArithmeticFunction.IsMultiplicative.mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) a : ℤ) ((1 : (a : ℕ) → ℤ) a : ℤ)
hb' : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) b : ℤ) ((1 : (a : ℕ) → ℤ) b : ℤ)
⊢ (μ * (↑ζ : ArithmeticFunction ℤ)).IsMultiplicative

Tactic:
exact isMultiplicative_moebius.mul isMultiplicative_zeta.natCast

Premises used: ArithmeticFunction.IsMultiplicative.natCast, ArithmeticFunction.isMultiplicative_zeta, ArithmeticFunction.isMultiplicative_moebius, ArithmeticFunction.IsMultiplicative.mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)
h₁ : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 1 : ℤ) ((1 : (a : ℕ) → ℤ) 1 : ℤ)
h₂ :
  ∀ (p n : ℕ) (hp : Nat.Prime p) (hn : 0 < n),
    Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) (p ^ n) : ℤ) ((1 : (a : ℕ) → ℤ) (p ^ n) : ℤ)
h₃ :
  ∀ (a b : ℕ) (_ha : 1 < a) (_hb : 1 < b) (hab : a.Coprime b)
    (ha' : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) a : ℤ) ((1 : (a : ℕ) → ℤ) a : ℤ))
    (hb' : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) b : ℤ) ((1 : (a : ℕ) → ℤ) b : ℤ)),
    Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) (a * b) : ℤ) ((1 : (a : ℕ) → ℤ) (a * b) : ℤ)
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) n : ℤ) ((1 : (a : ℕ) → ℤ) n : ℤ)

Tactic:
induction n using recOnPosPrimePosCoprime with
  | zero => rw [map_zero, map_zero]
  | one => simp
  | prime_pow p n hp hn =>
    rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ']
    simp [moebius_apply_prime_pow, hp.ne_one, hn.ne', hp, hn]
  | coprime a b _ha _hb hab ha' hb' =>
    rw [IsMultiplicative.map_mul_of_coprime _ hab, ha', hb',
      IsMultiplicative.map_mul_of_coprime isMultiplicative_one hab]
    exact isMultiplicative_moebius.mul isMultiplicative_zeta.natCast

Premises used: ArithmeticFunction.zero, ArithmeticFunction.IsMultiplicative.natCast, ArithmeticFunction.moebius_apply_prime_pow, ArithmeticFunction.isMultiplicative_zeta, ArithmeticFunction.map_zero, ArithmeticFunction.coe_mul_zeta_apply, ArithmeticFunction.isMultiplicative_moebius, ArithmeticFunction.IsMultiplicative.mul, ArithmeticFunction.one, Finset.sum_range_succ'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
rw : μ * (↑ζ : ArithmeticFunction ℤ) = 1
rw₁ rw₂ : Eq (α := ArithmeticFunction ℤ) 1 1
⊢ (↑ζ : ArithmeticFunction ℤ) * μ = 1

Tactic:
rw [mul_comm, moebius_mul_coe_zeta]

Premises used: ArithmeticFunction.moebius_mul_coe_zeta, mul_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : Ring R
rw :
  HMul.hMul (α := ArithmeticFunction R) (↑μ : ArithmeticFunction R)
      (↑(↑ζ : ArithmeticFunction ℤ) : ArithmeticFunction R) =
    1
rw₁ : Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑(μ * (↑ζ : ArithmeticFunction ℤ)) : ArithmeticFunction R) 1
rw₂ : Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑1 : ArithmeticFunction R) 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := ArithmeticFunction R) 1 1
⊢ HMul.hMul (α := ArithmeticFunction R) (↑μ : ArithmeticFunction R) (↑ζ : ArithmeticFunction R) = 1

Tactic:
rw [← coe_coe, ← intCoe_mul, moebius_mul_coe_zeta, intCoe_one]

Premises used: ArithmeticFunction.intCoe_one, ArithmeticFunction.coe_coe, ArithmeticFunction.moebius_mul_coe_zeta, ArithmeticFunction.intCoe_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : Ring R
rw :
  HMul.hMul (α := ArithmeticFunction R) (↑(↑ζ : ArithmeticFunction ℤ) : ArithmeticFunction R)
      (↑μ : ArithmeticFunction R) =
    1
rw₁ : Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑((↑ζ : ArithmeticFunction ℤ) * μ) : ArithmeticFunction R) 1
rw₂ : Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑1 : ArithmeticFunction R) 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := ArithmeticFunction R) 1 1
⊢ HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) (↑μ : ArithmeticFunction R) = 1

Tactic:
rw [← coe_coe, ← intCoe_mul, coe_zeta_mul_moebius, intCoe_one]

Premises used: ArithmeticFunction.intCoe_one, ArithmeticFunction.coe_coe, ArithmeticFunction.intCoe_mul, ArithmeticFunction.coe_zeta_mul_moebius
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑zetaUnit : ArithmeticFunction R) (↑ζ : ArithmeticFunction R)

Tactic:
rfl

Premises used: ArithmeticFunction.natToArithmeticFunction, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑zetaUnit⁻¹ : ArithmeticFunction R) (↑μ : ArithmeticFunction R)

Tactic:
rfl

Premises used: ArithmeticFunction.ofInt, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
trans :
  (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g'
trans₁ :
  HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g' ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n

Tactic:
trans (ζ : ArithmeticFunction ℤ) • f' = g'

Premises used: ArithmeticFunction.zeta, ArithmeticFunction.natToArithmeticFunction
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
rw :
  (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ (x : ℕ),
      Eq (α := R) ((HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' : (a : ℕ) → R) x : R)
        ((g' : (a : ℕ) → R) x : R)
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g'

Tactic:
rw [ArithmeticFunction.ext_iff]

Premises used: ArithmeticFunction.ext_iff