awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
h : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1
n : ℕ
pos :
  ∀ (hn : Nat.Prime n),
    Set.indicator {n : ℕ | Nat.Prime n} (term (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1) n =
      -(↑(Set.indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n) : ℂ)
neg :
  ∀ (hn : ¬Nat.Prime n),
    Set.indicator {n : ℕ | Nat.Prime n} (term (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1) n =
      -(↑(Set.indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n) : ℂ)
⊢ Set.indicator {n : ℕ | Nat.Prime n} (term (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1) n =
    -(↑(Set.indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n) : ℂ)

Tactic:
by_cases hn : n.Prime

Premises used: Nat.Prime
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
h : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1
n : ℕ
hn : Nat.Prime n
⊢ Set.indicator {n : ℕ | Nat.Prime n} (term (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1) n =
    -(↑(Set.indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n) : ℂ)

Tactic:
simp [hn, hn.ne_zero, moebius_apply_prime hn, push_cast, neg_div]

Premises used: neg_div, ArithmeticFunction.moebius_apply_prime, Nat.Prime.ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
h : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1
n : ℕ
hn : ¬Nat.Prime n
⊢ Set.indicator {n : ℕ | Nat.Prime n} (term (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) 1) n =
    -(↑(Set.indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n) : ℂ)

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
⊢ LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s ↔ 1 < s.re

Tactic:
⟨fun H ↦ ?_, LSeriesSummable_of_bounded_of_one_lt_re (m := 1) fun n _ ↦ ?_⟩

Premises used: LSeriesSummable_of_bounded_of_one_lt_re, Iff.intro
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
refine_1 : ∀ (H : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s), 1 < s.re
refine_2 : ∀ (n : ℕ), n ≠ 0 → norm (E := ℂ) (↑((μ : (a : ℕ) → ℤ) n) : ℂ) ≤ 1
⊢ LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s ↔ 1 < s.re

Tactic:
refine ⟨fun H ↦ ?_, LSeriesSummable_of_bounded_of_one_lt_re (m := 1) fun n _ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
H : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s
refine_1 : ∀ (h : s.re ≤ 1), False
⊢ 1 < s.re

Tactic:
by_contra! h
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
H : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s
h : s.re ≤ 1
⊢ s.re ≤ re 1

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
H : LSeriesSummable (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s
h : s.re ≤ 1
⊢ False

Tactic:
exact not_LSeriesSummable_moebius_at_one <| LSeriesSummable.of_re_le_re (by simpa) H

Premises used: ArithmeticFunction.not_LSeriesSummable_moebius_at_one, LSeriesSummable.of_re_le_re
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
n : ℕ
h : n ≠ 0
refine_2 : LE.le (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)
⊢ norm (E := ℂ) (↑((μ : (a : ℕ) → ℤ) n) : ℂ) ≤ 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
n : ℕ
h : n ≠ 0
⊢ LE.le (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)

Tactic:
abs_moebius_le_one

Premises used: ArithmeticFunction.abs_moebius_le_one
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
s : ℂ
n : ℕ
h : n ≠ 0
⊢ LE.le (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)

Tactic:
exact abs_moebius_le_one

Premises used: ArithmeticFunction.abs_moebius_le_one
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) = 1

Tactic:
simpa [abscissaOfAbsConv, LSeriesSummable_moebius_iff, Set.Ioi_def, EReal.image_coe_Ioi]
    using csInf_Ioo <| EReal.coe_lt_top 1

Premises used: csInf_Ioo, ArithmeticFunction.LSeriesSummable_moebius_iff, OfNat.ofNat, EReal.image_coe_Ioi, EReal.coe_lt_top, Set.Ioi_def, LSeries.abscissaOfAbsConv
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : AddMonoidWithOne R
n : ℕ
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := R) (1 n) (↑((fun (x : ℕ) ↦ ((ζ : (a : ℕ) → ℕ) x : ℕ)) n) : R)

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : Semiring R
f : ℕ → R
⊢ 1 ⍟ f = (fun (x : ℕ) ↦ (↑((ArithmeticFunction.zeta : (a : ℕ) → ℕ) x) : R)) ⍟ f

Tactic:
convolution_congr ArithmeticFunction.const_one_eq_zeta fun _ ↦ rfl

Premises used: LSeries.convolution_congr, ArithmeticFunction.const_one_eq_zeta, rfl
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : Semiring R
f : ℕ → R
⊢ f ⍟ 1 = f ⍟ fun (x : ℕ) ↦ (↑((ArithmeticFunction.zeta : (a : ℕ) → ℕ) x) : R)

Tactic:
convolution_congr (fun _ ↦ rfl) ArithmeticFunction.const_one_eq_zeta

Premises used: LSeries.convolution_congr, ArithmeticFunction.const_one_eq_zeta, rfl
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R N
⊢ IsMultiplicative.{u_1} (R := R) (toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N))

Tactic:
IsMultiplicative.iff_ne_zero.mpr ⟨?_, fun {m} {n} hm hn _ ↦ ?_⟩

Premises used: Iff.mpr, And.intro, ArithmeticFunction.IsMultiplicative.iff_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R N
refine_1 :
  Eq.{u_1 + 1} (α := R) ((toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N) : (a : ℕ) → R) 1 : R)
    (1 : R)
refine_2 :
  ∀ {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0),
    m.Coprime n →
      (toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N) : (a : ℕ) → R) (m * n) =
        HMul.hMul (α := R) (β := R)
          ((toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N) : (a : ℕ) → R) m : R)
          ((toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N) : (a : ℕ) → R) n : R)
⊢ IsMultiplicative.{u_1} (R := R) (toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N))

Tactic:
refine IsMultiplicative.iff_ne_zero.mpr ⟨?_, fun {m} {n} hm hn _ ↦ ?_⟩

Premises used: Iff.mpr, And.intro, ArithmeticFunction.IsMultiplicative.iff_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R N
⊢ Eq.{u_1 + 1} (α := R) ((toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N) : (a : ℕ) → R) 1 : R)
    (1 : R)

Tactic:
simp [toArithmeticFunction]

Premises used: toArithmeticFunction
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R N
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
h : m.Coprime n
⊢ (toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N) : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R)
      ((toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N) : (a : ℕ) → R) m : R)
      ((toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N) : (a : ℕ) → R) n : R)

Tactic:
simp [toArithmeticFunction, hm, hn]

Premises used: toArithmeticFunction
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R N
n : ℕ
hn : n ≠ 0
⊢ Eq (α := R) ((χ : (a : ZMod N) → R) (↑n : ZMod N) : R)
    ((toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → R) (↑x : ZMod N) : (a : ℕ) → R) n : R)

Tactic:
simp [toArithmeticFunction, hn]

Premises used: toArithmeticFunction
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
χ : DirichletCharacter R n
f g : ℕ → R
h :
  ∀ (n_1 : ℕ),
    ((fun (x : ℕ) ↦ (χ : (a : ZMod n) → R) (↑x : ZMod n)) * f ⍟
          ((fun (x : ℕ) ↦ (χ : (a : ZMod n) → R) (↑x : ZMod n)) * g))
        n_1 =
      HMul.hMul (α := ℕ → R) (fun (x : ℕ) ↦ (χ : (a : ZMod n) → R) (↑x : ZMod n)) (f ⍟ g) n_1
⊢ (fun (x : ℕ) ↦ (χ : (a : ZMod n) → R) (↑x : ZMod n)) * f ⍟
      ((fun (x : ℕ) ↦ (χ : (a : ZMod n) → R) (↑x : ZMod n)) * g) =
    (fun (x : ℕ) ↦ (χ : (a : ZMod n) → R) (↑x : ZMod n)) * (f ⍟ g)

Tactic:
ext n
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : ℕ
χ : DirichletCharacter R n_1
f g : ℕ → R
n : ℕ
h :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑x.1 : ZMod n_1) : R) (f x.1) *
        HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑x.2 : ZMod n_1) : R) (g x.2))
    (∑ i ∈ n.divisorsAntidiagonal, HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑n : ZMod n_1) : R) (f i.1 * g i.2))
⊢ ((fun (x : ℕ) ↦ (χ : (a : ZMod n_1) → R) (↑x : ZMod n_1)) * f ⍟
        ((fun (x : ℕ) ↦ (χ : (a : ZMod n_1) → R) (↑x : ZMod n_1)) * g))
      n =
    HMul.hMul (α := ℕ → R) (fun (x : ℕ) ↦ (χ : (a : ZMod n_1) → R) (↑x : ZMod n_1)) (f ⍟ g) n

Tactic:
simp only [Pi.mul_apply, LSeries.convolution_def, Finset.mul_sum]

Premises used: Finset.mul_sum, Pi.mul_apply, LSeries.convolution_def
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : ℕ
χ : DirichletCharacter R n_1
f g : ℕ → R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑x.1 : ZMod n_1) : R) (f x.1) *
        HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑x.2 : ZMod n_1) : R) (g x.2))
    (∑ i ∈ n.divisorsAntidiagonal, HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑n : ZMod n_1) : R) (f i.1 * g i.2))

Tactic:
Finset.sum_congr rfl fun p hp ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : ℕ
χ : DirichletCharacter R n_1
f g : ℕ → R
n : ℕ
h :
  ∀ (p : ℕ × ℕ) (hp : p ∈ n.divisorsAntidiagonal),
    HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R) (f p.1) *
        HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) (g p.2) =
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑n : ZMod n_1) : R) (f p.1 * g p.2)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑x.1 : ZMod n_1) : R) (f x.1) *
        HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑x.2 : ZMod n_1) : R) (g x.2))
    (∑ i ∈ n.divisorsAntidiagonal, HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑n : ZMod n_1) : R) (f i.1 * g i.2))

Tactic:
refine Finset.sum_congr rfl fun p hp ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : ℕ
χ : DirichletCharacter R n_1
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
h :
  HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R) (f p.1) *
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) (g p.2) =
    HMul.hMul (α := R) (β := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R)
        ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) *
      (f p.1 * g p.2)
⊢ HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R) (f p.1) *
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) (g p.2) =
    HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑n : ZMod n_1) : R) (f p.1 * g p.2)

Tactic:
rw [(mem_divisorsAntidiagonal.mp hp).1.symm, cast_mul, map_mul]

Premises used: Nat.mem_divisorsAntidiagonal, map_mul, Nat.cast_mul, And.left, Iff.mp, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : ℕ
χ : DirichletCharacter R n_1
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R) (f p.1) *
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) (g p.2) =
    HMul.hMul (α := R) (β := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R)
        ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) *
      (f p.1 * g p.2)

Tactic:
mul_mul_mul_comm ..

Premises used: mul_mul_mul_comm
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : ℕ
χ : DirichletCharacter R n_1
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R) (f p.1) *
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) (g p.2) =
    HMul.hMul (α := R) (β := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R)
        ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) *
      (f p.1 * g p.2)

Tactic:
exact mul_mul_mul_comm ..

Premises used: mul_mul_mul_comm
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
rw : Eq (α := ℂ) ((χ : (a : ZMod n) → ℂ) 1 : ℂ) (1 : ℂ)
rw₁ rw₂ : Eq (α := ℂ) 1 1
⊢ Eq (α := ℂ) ((χ : (a : ZMod n) → ℂ) (↑1 : ZMod n) : ℂ) (1 : ℂ)

Tactic:
rw [cast_one, map_one]

Premises used: map_one, Nat.cast_one
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ (δ * fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) = δ

Tactic:
mul_comm δ _ ▸ mul_delta ..

Premises used: LSeries.delta, DirichletCharacter.mul_delta, Eq.rec, mul_comm, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
rw :
  Eq (α := ℕ → ℂ) ((fun (x : ℕ) ↦ (↑((zeta : (a : ℕ) → ℕ) x) : ℂ)) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
⊢ (1 ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ)) = δ

Tactic:
rw [one_convolution_eq_zeta_convolution, ← one_eq_delta]

Premises used: ArithmeticFunction.one_eq_delta, LSeries.one_convolution_eq_zeta_convolution
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
simp_rw :
  Eq (α := ℕ → ℂ)
    ((fun (x : ℕ) ↦ ((↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
simp_rw₁ :
  Eq (α := ℕ → ℂ)
    ((fun (x : ℕ) ↦ ((↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x) ⍟ fun (x : ℕ) ↦
      ((↑μ : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x)
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
simp_rw₂ :
  Eq (α := ℕ → ℂ)
    (⇑(HMul.hMul (α := ArithmeticFunction ℂ) (↑zeta : ArithmeticFunction ℂ) (↑μ : ArithmeticFunction ℂ)) : (a : ℕ) → ℂ)
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
⊢ Eq (α := ℕ → ℂ) ((fun (x : ℕ) ↦ (↑((zeta : (a : ℕ) → ℕ) x) : ℂ)) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n

Tactic:
simp_rw [← natCoe_apply, ← intCoe_apply, coe_mul, coe_zeta_mul_coe_moebius]

Premises used: ArithmeticFunction.coe_mul, ArithmeticFunction.coe_zeta_mul_coe_moebius, ArithmeticFunction.natCoe_apply, ArithmeticFunction.intCoe_apply
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ (1 ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ)) = δ

Tactic:
have : (1 : ℕ → ℂ) ⍟ (μ ·) = δ := by
    rw [one_convolution_eq_zeta_convolution, ← one_eq_delta]
    simp_rw [← natCoe_apply, ← intCoe_apply, coe_mul, coe_zeta_mul_coe_moebius]
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ)) = δ
nth_rewrite :
  (HMul.hMul (α := ℕ → ℂ) (fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) 1 ⍟
      HMul.hMul (α := ℕ → ℂ) (fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) fun (n : ℕ) ↦
        (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) =
    δ
⊢ ((fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) ⍟
      HMul.hMul (α := ℕ → ℂ) (fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) fun (n : ℕ) ↦
        (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) =
    δ

Tactic:
nth_rewrite 1 [← mul_one ↗χ]

Premises used: Nat.cast, mul_one, DFunLike.coe
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ)) = δ
⊢ (HMul.hMul (α := ℕ → ℂ) (fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) 1 ⍟
      HMul.hMul (α := ℕ → ℂ) (fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) fun (n : ℕ) ↦
        (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) =
    δ

Tactic:
simpa only [mul_convolution_distrib χ 1 ↗μ, this] using mul_delta _

Premises used: Int.cast, DirichletCharacter.mul_delta, DirichletCharacter.mul_convolution_distrib, ArithmeticFunction.moebius, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
χ : DirichletCharacter ℂ 0
h : ∀ (n : ℕ), (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
⊢ (fun (n : ℕ) ↦ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0)) = δ

Tactic:
ext n
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
χ : DirichletCharacter ℂ 0
n : ℕ
h : (χ : (a : ZMod 0) → ℂ) (↑0 : ZMod 0) = δ 0
h₁ : ∀ (hn : n ≠ 0), (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
⊢ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
χ : DirichletCharacter ℂ 0
h : (χ : (a : ZMod 0) → ℂ) 0 = δ 0
h₁ : 0 = δ 0
h₂ : Eq (α := ℂ) 0 (if Eq (α := ℕ) 0 1 then 1 else 0)
h₃ : Eq (α := ℂ) 0 (if False then 1 else 0)
⊢ (χ : (a : ZMod 0) → ℂ) (↑0 : ZMod 0) = δ 0

Tactic:
simp_rw [cast_zero, χ.map_nonunit not_isUnit_zero, delta, reduceCtorEq, if_false]

Premises used: reduceCtorEq, LSeries.delta, if_false, not_isUnit_zero, MulChar.map_nonunit, Nat.cast_zero
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
h : ∀ (hn : Ne (α := ℕ) 1 0), (χ : (a : ZMod 0) → ℂ) (↑1 : ZMod 0) = δ 1
h₁ : ∀ (hn' : n ≠ 1), (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
⊢ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n

Tactic:
rcases eq_or_ne n 1 with rfl | hn'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
χ : DirichletCharacter ℂ 0
hn : Ne (α := ℕ) 1 0
⊢ (χ : (a : ZMod 0) → ℂ) (↑1 : ZMod 0) = δ 1

Tactic:
simp [delta]

Premises used: LSeries.delta
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
⊢ ¬IsUnit (M := ZMod 0) (↑n : ZMod 0)

Tactic:
have : ¬ IsUnit (n : ZMod 0) := fun h ↦ hn' <| ZMod.eq_one_of_isUnit_natCast h
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
this : ¬IsUnit (M := ZMod 0) (↑n : ZMod 0)
⊢ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n

Tactic:
simp_all [χ.map_nonunit this, delta]

Premises used: LSeries.delta, MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
h : ∀ (x : ℕ), Eq (α := R) ((χ : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (fun (x : ℕ) ↦ (χ : (a : ZMod 1) → R) (↑x : ZMod 1)) 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
x : ℕ
h : Eq.{u_1 + 1} (α := R) ((1 : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)
h₁ : Eq.{u_1 + 1} (α := R) 1 (1 x)
h₂ h₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq (α := R) ((χ : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)

Tactic:
rw [χ.level_one, MulChar.one_apply (isUnit_of_subsingleton _), Pi.one_apply]

Premises used: Pi.one_apply, DirichletCharacter.level_one, MulChar.one_apply, isUnit_of_subsingleton
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
⊢ (L fun (n : ℕ) ↦ (1 : (a : ZMod 1) → ℂ) (↑n : ZMod 1)) = L 1

Tactic:
congr_arg L modOne_eq_one

Premises used: DirichletCharacter.modOne_eq_one, LSeries, congr_arg
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ ¬LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1

Tactic:
fun h ↦ (Real.not_summable_indicator_one_div_natCast hN 1) ?_

Premises used: Real.not_summable_indicator_one_div_natCast, OfNat.ofNat, Not
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
refine :
  ∀ (h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1),
    Summable (α := ℝ)
      (Set.indicator {n : ℕ | Eq (α := ZMod N) (↑n : ZMod N) 1} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ ¬LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1

Tactic:
refine fun h ↦ (Real.not_summable_indicator_one_div_natCast hN 1) ?_

Premises used: Real.not_summable_indicator_one_div_natCast, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
m : ℕ
h_1 : Membership.mem (γ := Set ℕ) {n : ℕ | Eq (α := ZMod N) (↑n : ZMod N) 1} m
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
refine :
  ∀ (n : ℕ),
    Set.indicator {n : ℕ | Eq (α := ZMod N) (↑n : ZMod N) 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n ≤
      ‖term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1 n‖
⊢ Summable (α := ℝ)
    (Set.indicator {n : ℕ | Eq (α := ZMod N) (↑n : ZMod N) 1} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
refine h.norm.of_nonneg_of_le (fun m ↦ Set.indicator_apply_nonneg (fun _ ↦ by positivity))
    (fun n ↦ ?_)

Premises used: Summable.of_nonneg_of_le, Summable.norm, Set.indicator_apply_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
simp :
  (if Eq (α := ZMod N) (↑n : ZMod N) 1 then HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) else 0) ≤
    if n = 0 then 0 else norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
⊢ Set.indicator {n : ℕ | Eq (α := ZMod N) (↑n : ZMod N) 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n ≤
    ‖term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1 n‖

Tactic:
simp only [norm_term_eq, Set.indicator, Set.mem_setOf_eq]

Premises used: Set.indicator, Set.mem_setOf_eq, LSeries.norm_term_eq
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
pos : ∀ (h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1) (h₂ : n = 0), HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ 0
neg :
  ∀ (h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1) (h₂ : ¬n = 0),
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
      norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
pos₁ : ∀ (h₁ : ¬Eq (α := ZMod N) (↑n : ZMod N) 1), n = 0 → LE.le (α := ℝ) 0 0
neg₁ :
  ∀ (h₁ : ¬Eq (α := ZMod N) (↑n : ZMod N) 1),
    ¬n = 0 → 0 ≤ norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
⊢ (if Eq (α := ZMod N) (↑n : ZMod N) 1 then HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) else 0) ≤
    if n = 0 then 0 else norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1
h₂ : n = 0
⊢ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ 0

Tactic:
simp [h₂]
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1
h₂ : ¬n = 0
⊢ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)

Tactic:
simp [h₁, χ.map_one]

Premises used: MulChar.map_one
-- Module: Mathlib.NumberTheory.LSeries.Dirichlet
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
h₁ : ¬Eq (α := ZMod N) (↑n : ZMod N) 1
h_1 : n = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
positivity