awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
hn : IsPrimePow n
hn' : ¬Nat.Prime n
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)
have obtain : ∀ (p k : ℕ) (hp : Nat.Prime p) (hk : 0 < k) (hn : IsPrimePow (p ^ k)) (hn' : ¬Nat.Prime (p ^ k)),
  Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (0 : ℤ)
Tactic: obtain ⟨p, k, hp, hk, rfl⟩ := (isPrimePow_nat_iff _).1 hn
Cleared hypotheses: n, hn, hn'
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (0 : ℤ)
have hnc : ¬k = 1
Tactic: rw [moebius_apply_prime_pow hp hk.ne', if_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
⊢ μ.IsMultiplicative
have rw : Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) 1 : ℤ) (1 : ℤ) ∧
  ∀ {m n : ℕ},
    m ≠ 0 →
      n ≠ 0 →
        m.Coprime n →
          (μ : (a : ℕ) → ℤ) (m * n) = HMul.hMul (α := ℤ) (β := ℤ) ((μ : (a : ℕ) → ℤ) m : ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ)
Tactic: rw [IsMultiplicative.iff_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) 1 : ℤ) (1 : ℤ) ∧
    ∀ {m n : ℕ},
      m ≠ 0 →
        n ≠ 0 →
          m.Coprime n →
            (μ : (a : ℕ) → ℤ) (m * n) = HMul.hMul (α := ℤ) (β := ℤ) ((μ : (a : ℕ) → ℤ) m : ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ)
have refine : ∀ {n m : ℕ} (hn : n ≠ 0) (hm : m ≠ 0) (hnm : n.Coprime m),
  (μ : (a : ℕ) → ℤ) (n * m) = HMul.hMul (α := ℤ) (β := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) ((μ : (a : ℕ) → ℤ) m : ℤ)
Tactic: refine ⟨by simp, fun {n m} hn hm hnm => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
h_mult : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
⊢ 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)
have 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)
Tactic: trans (∏ᵖ p ∣ n, ((ζ : ArithmeticFunction R) + f) p)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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)
⊢ 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)
have 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)
Tactic: trans (∏ᵖ p ∣ n, ((ζ : ArithmeticFunction R) + f) p)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
h_mult : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
⊢ 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)
have 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))
Tactic: simp_rw [prodPrimeFactors_apply hn.ne_zero, add_apply, natCoe_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
h_mult : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
⊢ 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))
have 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)
Tactic: apply prod_congr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
    HAdd.hAdd (α := R) (β := R) ((↑((ζ : (a : ℕ) → ℕ) p) : R) : R) ((f : (a : ℕ) → R) p : R)
have rw : HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
  HAdd.hAdd (α := R) (β := R) ((↑1 : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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)
⊢ HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
    HAdd.hAdd (α := R) (β := R) ((↑((ζ : (a : ℕ) → ℕ) p) : R) : R) ((f : (a : ℕ) → R) p : R)
have rw₁ : HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R) =
  HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : ℕ) → R) p : R)
Tactic: rw [zeta_apply_ne (prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp).ne_zero, cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
h_mult : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
⊢ 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)
have rw : Eq (α := R)
  ((HMul.hMul (α := ArithmeticFunction R) ((↑ζ : ArithmeticFunction R) : ArithmeticFunction R) f : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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)
⊢ 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)
have rw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ n.divisors, (f : (a : ℕ) → R) i) (∑ d ∈ n.divisors, (f : (a : ℕ) → R) d)
Tactic: rw [isMultiplicative_zeta.natCast.prodPrimeFactors_add_of_squarefree h_mult hn,
    coe_zeta_mul_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
⊢ 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))
have 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))
Tactic: trans (∏ p ∈ n.primeFactors, (1 + (ArithmeticFunction.pmul (μ : ArithmeticFunction R) f) p))
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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))
⊢ 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))
have 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))
Tactic: trans (∏ p ∈ n.primeFactors, (1 + (ArithmeticFunction.pmul (μ : ArithmeticFunction R) f) p))
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
⊢ 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))
have 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)
Tactic: apply prod_congr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((ArithmeticFunction.pmul (↑μ : ArithmeticFunction R) f : (a : ℕ) → R) p : R)
have 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)
Tactic: rw [pmul_apply, intCoe_apply, ArithmeticFunction.moebius_apply_prime
        (prime_of_mem_primeFactorsList (List.mem_toFinset.mp hp))]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
⊢ 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))
have 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))
Tactic: rw [(isMultiplicative_moebius.intCast.pmul hf).prodPrimeFactors_one_add_of_squarefree hn]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
n : ℕ
hn : Squarefree n
⊢ 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))
have 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))
Tactic: simp_rw [pmul_apply, intCoe_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
⊢ μ * (↑ζ : ArithmeticFunction ℤ) = 1
have h : ∀ (n : ℕ), Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) n : ℤ) ((1 : (a : ℕ) → ℤ) n : ℤ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)
have h : Eq (α := ℤ) (0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
h : Eq (α := ℤ) (0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)
have h₁ : Eq (α := ℤ) 0 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) (p ^ n) : ℤ) ((1 : (a : ℕ) → ℤ) (p ^ n) : ℤ)
have h : HAdd.hAdd (α := ℤ) (β := ℤ) (∑ k ∈ range n, (μ : (a : ℕ) → ℤ) (p ^ (k + 1)) : ℤ)
    ((μ : (a : ℕ) → ℤ) (HPow.hPow (β := ℕ) p 0) : ℤ) =
  (1 : (a : ℕ) → ℤ) (p ^ n)
Tactic: rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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 : ℤ)
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) (a * b) : ℤ) ((1 : (a : ℕ) → ℤ) (a * b) : ℤ)
have rw : (μ * (↑ζ : ArithmeticFunction ℤ)).IsMultiplicative
Tactic: rw [IsMultiplicative.map_mul_of_coprime _ hab, ha', hb',
      IsMultiplicative.map_mul_of_coprime isMultiplicative_one hab]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) n : ℤ) ((1 : (a : ℕ) → ℤ) n : ℤ)
have h : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
h : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) n : ℤ) ((1 : (a : ℕ) → ℤ) n : ℤ)
have h₁ : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 1 : ℤ) ((1 : (a : ℕ) → ℤ) 1 : ℤ)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
h : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 0 : ℤ) ((1 : (a : ℕ) → ℤ) 0 : ℤ)
h₁ : Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) 1 : ℤ) ((1 : (a : ℕ) → ℤ) 1 : ℤ)
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) n : ℤ) ((1 : (a : ℕ) → ℤ) n : ℤ)
have h₂ : ∀ (p n : ℕ) (hp : Nat.Prime p) (hn : 0 < n),
  Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) (p ^ n) : ℤ) ((1 : (a : ℕ) → ℤ) (p ^ 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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) : ℤ)
⊢ Eq (α := ℤ) ((μ * (↑ζ : ArithmeticFunction ℤ) : (a : ℕ) → ℤ) n : ℤ) ((1 : (a : ℕ) → ℤ) n : ℤ)
have 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) : ℤ)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
⊢ (↑ζ : ArithmeticFunction ℤ) * μ = 1
have rw : μ * (↑ζ : ArithmeticFunction ℤ) = 1
Tactic: rw [mul_comm, moebius_mul_coe_zeta]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
rw : μ * (↑ζ : ArithmeticFunction ℤ) = 1
⊢ (↑ζ : ArithmeticFunction ℤ) * μ = 1
have rw₁ : Eq (α := ArithmeticFunction ℤ) 1 1
Tactic: rw [mul_comm, moebius_mul_coe_zeta]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : Ring R
⊢ HMul.hMul (α := ArithmeticFunction R) (↑μ : ArithmeticFunction R) (↑ζ : ArithmeticFunction R) = 1
have rw : HMul.hMul (α := ArithmeticFunction R) (↑μ : ArithmeticFunction R)
    (↑(↑ζ : ArithmeticFunction ℤ) : ArithmeticFunction R) =
  1
Tactic: rw [← coe_coe, ← intCoe_mul, moebius_mul_coe_zeta, intCoe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : Ring R
rw :
  HMul.hMul (α := ArithmeticFunction R) (↑μ : ArithmeticFunction R)
      (↑(↑ζ : ArithmeticFunction ℤ) : ArithmeticFunction R) =
    1
⊢ HMul.hMul (α := ArithmeticFunction R) (↑μ : ArithmeticFunction R) (↑ζ : ArithmeticFunction R) = 1
have rw₁ : Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑(μ * (↑ζ : ArithmeticFunction ℤ)) : ArithmeticFunction R) 1
Tactic: rw [← coe_coe, ← intCoe_mul, moebius_mul_coe_zeta, intCoe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HMul.hMul (α := ArithmeticFunction R) (↑μ : ArithmeticFunction R) (↑ζ : ArithmeticFunction R) = 1
have rw₂ : Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑1 : ArithmeticFunction R) 1
Tactic: rw [← coe_coe, ← intCoe_mul, moebius_mul_coe_zeta, intCoe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HMul.hMul (α := ArithmeticFunction R) (↑μ : ArithmeticFunction R) (↑ζ : ArithmeticFunction R) = 1
have rw₃ : Eq.{u_1 + 1} (α := ArithmeticFunction R) 1 1
Tactic: rw [← coe_coe, ← intCoe_mul, moebius_mul_coe_zeta, intCoe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : Ring R
⊢ HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) (↑μ : ArithmeticFunction R) = 1
have rw : HMul.hMul (α := ArithmeticFunction R) (↑(↑ζ : ArithmeticFunction ℤ) : ArithmeticFunction R)
    (↑μ : ArithmeticFunction R) =
  1
Tactic: rw [← coe_coe, ← intCoe_mul, coe_zeta_mul_moebius, intCoe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : Ring R
rw :
  HMul.hMul (α := ArithmeticFunction R) (↑(↑ζ : ArithmeticFunction ℤ) : ArithmeticFunction R)
      (↑μ : ArithmeticFunction R) =
    1
⊢ HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) (↑μ : ArithmeticFunction R) = 1
have rw₁ : Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑((↑ζ : ArithmeticFunction ℤ) * μ) : ArithmeticFunction R) 1
Tactic: rw [← coe_coe, ← intCoe_mul, coe_zeta_mul_moebius, intCoe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) (↑μ : ArithmeticFunction R) = 1
have rw₂ : Eq.{u_1 + 1} (α := ArithmeticFunction R) (↑1 : ArithmeticFunction R) 1
Tactic: rw [← coe_coe, ← intCoe_mul, coe_zeta_mul_moebius, intCoe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) (↑μ : ArithmeticFunction R) = 1
have rw₃ : Eq.{u_1 + 1} (α := ArithmeticFunction R) 1 1
Tactic: rw [← coe_coe, ← intCoe_mul, coe_zeta_mul_moebius, intCoe_one]