awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
        ((f : (a : ℕ) → M) x.2 : M))
    (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2)

Tactic:
sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
refine :
  ∀ (i : ℕ × ℕ) (hi : i ∈ x.divisorsAntidiagonal),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) i.1 : R)
        ((f : (a : ℕ) → M) i.2 : M) =
      (f : (a : ℕ) → M) i.2
⊢ Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
        ((f : (a : ℕ) → M) x.2 : M))
    (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2)

Tactic:
refine sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
⊢ i ∈ (i.1 * i.2).divisorsAntidiagonal

Tactic:
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩

Premises used: Nat.mem_divisorsAntidiagonal, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
hi₁ : i ∈ (i.1 * i.2).divisorsAntidiagonal
⊢ i.1 * i.2 ≠ 0

Tactic:
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩

Premises used: Nat.mem_divisorsAntidiagonal, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (↑((ζ : (a : ℕ) → ℕ) i.1) : R) ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (↑1 : R) ((f : (a : ℕ) → M) i.2 : M) = (f : (a : ℕ) → M) i.2
rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) 1 ((f : (a : ℕ) → M) i.2 : M) = (f : (a : ℕ) → M) i.2
rw₃ rw₄ : Eq (α := M) ((f : (a : ℕ) → M) i.2 : M) ((f : (a : ℕ) → M) i.2 : M)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) i.1 : R)
      ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2

Tactic:
rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]

Premises used: ArithmeticFunction.zeta_apply_ne, one_smul, left_ne_zero_of_mul, ArithmeticFunction.natCoe_apply, Nat.cast_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
rw :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ map { toFun := fun (d : ℕ) ↦ (x / d, d), inj' := ⋯ } x.divisors, (f : (a : ℕ) → M) i.2)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
rw₁ :
  Eq.{u_2 + 1} (α := M)
    (∑ x_1 ∈ x.divisors, (f : (a : ℕ) → M) (({ toFun := fun (d : ℕ) ↦ (x / d, d), inj' := ⋯ } : (a : ℕ) → ℕ × ℕ) x_1).2)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := M) (∑ x_1 ∈ x.divisors, (f : (a : ℕ) → M) (x / x_1, x_1).2) (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2) (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)

Tactic:
rw [← map_div_left_divisors, sum_map, Function.Embedding.coeFn_mk]

Premises used: Nat.map_div_left_divisors, Finset.sum_map, Function.Embedding.coeFn_mk
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      if x.1 = 0 then HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) 0 ((f : (a : ℕ) → M) x.2 : M)
      else (f : (a : ℕ) → M) x.2)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)

Tactic:
simp [← coe_zeta_smul_apply (R := R)]

Premises used: ArithmeticFunction.coe_zeta_smul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
h :
  ∀ (n : ℕ),
    Eq (α := R) ((HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) n : R)
      ((HMul.hMul (β := ArithmeticFunction R) f (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) n : R)
⊢ HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f =
    HMul.hMul (β := ArithmeticFunction R) f (↑ζ : ArithmeticFunction R)

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
n : ℕ
h :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.2 : R) ((↑((ζ : (a : ℕ) → ℕ) x.1) : R) : R))
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((↑((ζ : (a : ℕ) → ℕ) x.2) : R) : R))
⊢ Eq (α := R) ((HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) n : R)
    ((HMul.hMul (β := ArithmeticFunction R) f (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) n : R)

Tactic:
simp_rw [mul_apply, natCoe_apply, (cast_commute ..).eq]

Premises used: ArithmeticFunction.mul_apply, ArithmeticFunction.natCoe_apply, Commute.eq, Nat.cast_commute
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
n : ℕ
h :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ n.divisors, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (n / i) : R) ((↑((ζ : (a : ℕ) → ℕ) i) : R) : R))
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((↑((ζ : (a : ℕ) → ℕ) x.2) : R) : R))
h₁ h₂ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ n.divisors, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (n / i) : R) ((↑((ζ : (a : ℕ) → ℕ) i) : R) : R))
    (∑ i ∈ n.divisors, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (n / i) : R) ((↑((ζ : (a : ℕ) → ℕ) i) : R) : R))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.2 : R) ((↑((ζ : (a : ℕ) → ℕ) x.1) : R) : R))
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((↑((ζ : (a : ℕ) → ℕ) x.2) : R) : R))

Tactic:
rw [sum_divisorsAntidiagonal fun x y ↦ f y * ζ x, sum_divisorsAntidiagonal' fun x y ↦ f x * ζ y]

Premises used: HMul.hMul, ArithmeticFunction.zeta, Nat.cast, Nat.sum_divisorsAntidiagonal', DFunLike.coe, Nat.sum_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) ((HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) x : R)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i : R)

Tactic:
coe_zeta_smul_apply

Premises used: ArithmeticFunction.coe_zeta_smul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
rw :
  Eq (α := R) ((HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) x : R)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i : R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i) (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i)
⊢ Eq (α := R) ((HMul.hMul (β := ArithmeticFunction R) f (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x : R)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i : R)

Tactic:
rw [← coe_zeta_mul_comm, coe_zeta_mul_apply]

Premises used: ArithmeticFunction.coe_zeta_mul_comm, ArithmeticFunction.coe_zeta_mul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
f : ArithmeticFunction ℕ
x : ℕ
rw : Eq (α := ℕ) (((↑ζ : ArithmeticFunction ℕ) * f : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
rw₁ rw₂ : Eq (α := ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i)
⊢ Eq (α := ℕ) ((ζ * f : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)

Tactic:
rw [← natCoe_nat ζ, coe_zeta_mul_apply]

Premises used: ArithmeticFunction.zeta, ArithmeticFunction.natCoe_nat, ArithmeticFunction.coe_zeta_mul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
f : ArithmeticFunction ℕ
x : ℕ
rw : Eq (α := ℕ) ((f * (↑ζ : ArithmeticFunction ℕ) : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
rw₁ rw₂ : Eq (α := ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i)
⊢ Eq (α := ℕ) ((f * ζ : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)

Tactic:
rw [← natCoe_nat ζ, coe_mul_zeta_apply]

Premises used: ArithmeticFunction.zeta, ArithmeticFunction.coe_mul_zeta_apply, ArithmeticFunction.natCoe_nat
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
f : ArithmeticFunction ℕ
rw : (↑ζ : ArithmeticFunction ℕ) * f = f * (↑ζ : ArithmeticFunction ℕ)
rw₁ rw₂ : f * (↑ζ : ArithmeticFunction ℕ) = f * (↑ζ : ArithmeticFunction ℕ)
⊢ ζ * f = f * ζ

Tactic:
rw [← natCoe_nat ζ, coe_zeta_mul_comm]

Premises used: ArithmeticFunction.zeta, ArithmeticFunction.natCoe_nat, ArithmeticFunction.coe_zeta_mul_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : MulZeroClass R
f g : ArithmeticFunction R
⊢ Eq.{u_1 + 1} (α := R)
    ((fun (x : ℕ) ↦ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((g : (a : ℕ) → R) x : R)) 0) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : MulZeroClass R
f g : ArithmeticFunction R
x : ℕ
⊢ (f.pmul g : (a : ℕ) → R) x = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((g : (a : ℕ) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f g : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) ((f.pmul g : (a : ℕ) → R) x : R) ((g.pmul f : (a : ℕ) → R) x : R)
⊢ f.pmul g = g.pmul f

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f g : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) ((f.pmul g : (a : ℕ) → R) x : R) ((g.pmul f : (a : ℕ) → R) x : R)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : SemigroupWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) (((f₁.pmul f₂).pmul f₃ : (a : ℕ) → R) x : R) ((f₁.pmul (f₂.pmul f₃) : (a : ℕ) → R) x : R)
⊢ (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : SemigroupWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) (((f₁.pmul f₂).pmul f₃ : (a : ℕ) → R) x : R) ((f₁.pmul (f₂.pmul f₃) : (a : ℕ) → R) x : R)

Tactic:
simp only [pmul_apply, mul_assoc]

Premises used: ArithmeticFunction.pmul_apply, mul_assoc
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
⊢ f.pmul (↑ζ : ArithmeticFunction R) = f

Tactic:
ext x
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
h : Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)
h₁ :
  ∀ (n : ℕ),
    Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) (n + 1) : R) ((f : (a : ℕ) → R) (n + 1) : R)
⊢ Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)

Tactic:
cases x
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
⊢ Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
n : ℕ
⊢ Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) (n + 1) : R) ((f : (a : ℕ) → R) (n + 1) : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
⊢ pmul (↑ζ : ArithmeticFunction R) f = f

Tactic:
ext x
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
h : Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)
h₁ :
  ∀ (n : ℕ),
    Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) (n + 1) : R) ((f : (a : ℕ) → R) (n + 1) : R)
⊢ Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)

Tactic:
cases x
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
⊢ Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
n : ℕ
⊢ Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) (n + 1) : R) ((f : (a : ℕ) → R) (n + 1) : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
h0 : ¬k = 0
simp_rw simp_rw₁ : HPow.hPow (α := R) ((f : (a : ℕ) → R) 0 : R) k = 0
simp_rw₂ : HPow.hPow (α := R) 0 k = 0
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : ℕ) ↦ HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) 0) 0

Tactic:
simp_rw [map_zero, zero_pow h0]

Premises used: ArithmeticFunction.map_zero, zero_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
rw :
  Eq.{u_1 + 1} (α := ArithmeticFunction R)
    (if h0 : Eq (α := ℕ) 0 0 then (↑ζ : ArithmeticFunction R)
      else { toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0, map_zero' := ⋯ } :
      ArithmeticFunction R)
    (↑ζ : ArithmeticFunction R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := ArithmeticFunction R) ((↑ζ : ArithmeticFunction R) : ArithmeticFunction R)
    (↑ζ : ArithmeticFunction R)
⊢ f.ppow 0 = (↑ζ : ArithmeticFunction R)

Tactic:
rw [ppow, dif_pos rfl]

Premises used: dif_pos, ArithmeticFunction.ppow, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) ((f.ppow 1 : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
⊢ f.ppow 1 = f

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) ((f.ppow 1 : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)

Tactic:
simp [ppow]

Premises used: ArithmeticFunction.ppow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
rw :
  (if h0 : k = 0 then (↑ζ : ArithmeticFunction R)
        else { toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k, map_zero' := ⋯ } :
        (a : ℕ) → R)
      x =
    HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
rw₁ :
  ({ toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k, map_zero' := ⋯ } : (a : ℕ) → R) x =
    HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
rw₂ rw₃ : HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k = HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
⊢ (f.ppow k : (a : ℕ) → R) x = HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k

Tactic:
rw [ppow, dif_neg (Nat.ne_of_gt kpos), coe_mk]

Premises used: ArithmeticFunction.coe_mk, ArithmeticFunction.ppow, dif_neg, Nat.ne_of_gt
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
h : ∀ (x : ℕ), Eq (α := R) ((f.ppow (k + 1) : (a : ℕ) → R) x : R) ((f.pmul (f.ppow k) : (a : ℕ) → R) x : R)
⊢ f.ppow (k + 1) = f.pmul (f.ppow k)

Tactic:
ext x
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k x : ℕ
h :
  HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) =
    (f.pmul (f.ppow k) : (a : ℕ) → R) x
⊢ Eq (α := R) ((f.ppow (k + 1) : (a : ℕ) → R) x : R) ((f.pmul (f.ppow k) : (a : ℕ) → R) x : R)

Tactic:
rw [ppow_apply (succ_pos k), _root_.pow_succ']

Premises used: ArithmeticFunction.ppow_apply, Nat.succ_pos, pow_succ'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k x : ℕ
h :
  HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0) =
    (f.pmul (f.ppow 0) : (a : ℕ) → R) x
h₁ :
  ∀ (n : ℕ),
    HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) n) =
        (f.pmul (f.ppow n) : (a : ℕ) → R) x →
      HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) (n + 1)) =
        (f.pmul (f.ppow (n + 1)) : (a : ℕ) → R) x
⊢ HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) =
    (f.pmul (f.ppow k) : (a : ℕ) → R) x

Tactic:
induction k
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0) =
    (f.pmul (f.ppow 0) : (a : ℕ) → R) x

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x n : ℕ
h :
  HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) n) =
    (f.pmul (f.ppow n) : (a : ℕ) → R) x
⊢ HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) (n + 1)) =
    (f.pmul (f.ppow (n + 1)) : (a : ℕ) → R) x

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
h : ∀ (x : ℕ), Eq (α := R) ((f.ppow (k + 1) : (a : ℕ) → R) x : R) (((f.ppow k).pmul f : (a : ℕ) → R) x : R)
⊢ f.ppow (k + 1) = (f.ppow k).pmul f

Tactic:
ext x
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
h :
  HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) ((f : (a : ℕ) → R) x : R) =
    ((f.ppow k).pmul f : (a : ℕ) → R) x
⊢ Eq (α := R) ((f.ppow (k + 1) : (a : ℕ) → R) x : R) (((f.ppow k).pmul f : (a : ℕ) → R) x : R)

Tactic:
rw [ppow_apply (succ_pos k), _root_.pow_succ]

Premises used: pow_succ, ArithmeticFunction.ppow_apply, Nat.succ_pos
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
h :
  ∀ {kpos : LT.lt (α := ℕ) 0 0},
    HMul.hMul (β := R) (HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0) ((f : (a : ℕ) → R) x : R) =
      ((f.ppow 0).pmul f : (a : ℕ) → R) x
h₁ :
  ∀ (n : ℕ),
    (∀ {kpos : 0 < n},
        HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) n) ((f : (a : ℕ) → R) x : R) =
          ((f.ppow n).pmul f : (a : ℕ) → R) x) →
      ∀ {kpos : 0 < n + 1},
        HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) (n + 1)) ((f : (a : ℕ) → R) x : R) =
          ((f.ppow (n + 1)).pmul f : (a : ℕ) → R) x
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) ((f : (a : ℕ) → R) x : R) =
    ((f.ppow k).pmul f : (a : ℕ) → R) x

Tactic:
induction k
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
kpos : LT.lt (α := ℕ) 0 0
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0) ((f : (a : ℕ) → R) x : R) =
    ((f.ppow 0).pmul f : (a : ℕ) → R) x

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x n : ℕ
h :
  ∀ {kpos : 0 < n},
    HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) n) ((f : (a : ℕ) → R) x : R) =
      ((f.ppow n).pmul f : (a : ℕ) → R) x
kpos : 0 < n + 1
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) (n + 1)) ((f : (a : ℕ) → R) x : R) =
    ((f.ppow (n + 1)).pmul f : (a : ℕ) → R) x

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : GroupWithZero R
f g : ArithmeticFunction R
⊢ Eq.{u_1 + 1} (α := R)
    ((fun (n : ℕ) ↦ HDiv.hDiv (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)) 0) 0

Tactic:
simp only [map_zero, div_zero]

Premises used: ArithmeticFunction.map_zero, div_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : GroupWithZero R
f g : ArithmeticFunction R
n : ℕ
⊢ (f.pdiv g : (a : ℕ) → R) n = HDiv.hDiv (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : DivisionSemiring R
f : ArithmeticFunction R
h : ∀ (n : ℕ), Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) n : R) ((f : (a : ℕ) → R) n : R)
⊢ f.pdiv (↑ζ : ArithmeticFunction R) = f

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : DivisionSemiring R
f : ArithmeticFunction R
n : ℕ
h : Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)
h₁ :
  ∀ (n : ℕ),
    Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) (n + 1) : R) ((f : (a : ℕ) → R) (n + 1) : R)
⊢ Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) n : R) ((f : (a : ℕ) → R) n : R)

Tactic:
cases n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : DivisionSemiring R
f : ArithmeticFunction R
⊢ Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : DivisionSemiring R
f : ArithmeticFunction R
n : ℕ
⊢ Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) (n + 1) : R) ((f : (a : ℕ) → R) (n + 1) : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
⊢ Eq (α := ℕ) ((ζ : (a : ℕ) → ℕ) 1 : ℕ) (1 : ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
⊢ ∀ {m n : ℕ},
    m ≠ 0 →
      n ≠ 0 →
        m.Coprime n →
          (ζ : (a : ℕ) → ℕ) (m * n) = HMul.hMul (α := ℕ) (β := ℕ) ((ζ : (a : ℕ) → ℕ) m : ℕ) ((ζ : (a : ℕ) → ℕ) n : ℕ)

Tactic:
simp +contextual
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
⊢ Eq (α := R) ((f.pmul g : (a : ℕ) → R) 1 : R) (1 : R)

Tactic:
simp [hf, hg]