awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
⊢ Eq.{u_1 + 1} (α := (p : Primes) → F)
    (fun (p : Primes) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) (↑p : ℕ) : F))⁻¹) fun (p : Primes) ↦
    ∑' (e : ℕ), (f : (a : ℕ) → F) ((↑p : ℕ) ^ e)

Tactic:
have H : (fun p : Primes ↦ (1 - f p)⁻¹) = fun p : Primes ↦ ∑' (e : ℕ), f (p ^ e) :=
    funext <| fun p ↦ one_sub_inv_eq_geometric_of_summable_norm p.prop hsum
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
H :
  Eq.{u_1 + 1} (α := (p : Primes) → F)
    (fun (p : Primes) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) (↑p : ℕ) : F))⁻¹) fun (p : Primes) ↦
    ∑' (e : ℕ), (f : (a : ℕ) → F) ((↑p : ℕ) ^ e)
⊢ HasProd.{u_1, 0} (α := F)
    (fun (p : Primes) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) (↑p : ℕ) : F))⁻¹)
    (∑' (n : ℕ), (f : (a : ℕ) → F) n)

Tactic:
simpa only [map_pow, H]
    using eulerProduct_hasProd f.map_one (fun {m n} _ ↦ f.map_mul m n) hsum f.map_zero

Premises used: MonoidWithZeroHom.map_one, EulerProduct.eulerProduct_hasProd, MonoidWithZeroHom.map_zero, map_pow, MonoidWithZeroHom.map_mul
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
⊢ Eq.{u_1 + 1} (α := F) (∏' (p : Primes), (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) (↑p : ℕ) : F))⁻¹)
    (∑' (n : ℕ), (f : (a : ℕ) → F) n)

Tactic:
(eulerProduct_completely_multiplicative_hasProd hsum).tprod_eq

Premises used: HasProd.tprod_eq, EulerProduct.eulerProduct_completely_multiplicative_hasProd
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
⊢ ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)

Tactic:
have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
⊢ Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦
      ∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} (fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e)) i)
    atTop (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))

Tactic:
have := (eulerProduct_hasProd_mulIndicator f.map_one hmul hsum f.map_zero).tendsto_prod_nat
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
this :
  Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦
      ∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} (fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e)) i)
    atTop (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
⊢ ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := F)
      (∏ p ∈ range n,
        Set.mulIndicator {p : ℕ | Nat.Prime p}
          (fun (p : ℕ) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) p)
      (∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)

Tactic:
have H (n : ℕ) : ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p =
                     ∏ p ∈ primesBelow n, (1 - f p)⁻¹ :=
    prod_mulIndicator_eq_prod_filter
      (range n) (fun _ ↦ fun p ↦ (1 - f p)⁻¹) (fun _ ↦ {p | Nat.Prime p}) id
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
this :
  Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦
      ∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} (fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e)) i)
    atTop (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
H :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := F)
      (∏ p ∈ range n,
        Set.mulIndicator {p : ℕ | Nat.Prime p}
          (fun (p : ℕ) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) p)
      (∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
⊢ Eq.{u_1 + 1} (α := (x : ℕ) → F)
    (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦
      (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e))

Tactic:
have H' : {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) =
              {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' e : ℕ, f (p ^ e)) :=
    Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
hmul :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
this :
  Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦
      ∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} (fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e)) i)
    atTop (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))
H :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := F)
      (∏ p ∈ range n,
        Set.mulIndicator {p : ℕ | Nat.Prime p}
          (fun (p : ℕ) ↦ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) p)
      (∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
H' :
  Eq.{u_1 + 1} (α := (x : ℕ) → F)
    (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦
      (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦ ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e))
⊢ Tendsto.{0, u_1} (β := F)
    (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹) atTop
    (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → F) n))

Tactic:
simpa only [← H, H'] using this
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : s ≠ 0
⊢ HPow.hPow (α := ℂ) (↑0 : ℂ) (-s) = 0

Tactic:
simp [hs]
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : s ≠ 0
⊢ HPow.hPow (α := ℂ) (↑1 : ℂ) (-s) = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : s ≠ 0
m n : ℕ
⊢ HPow.hPow (α := ℂ) (↑(m * n) : ℂ) (-s) = HPow.hPow (α := ℂ) (↑m : ℂ) (-s) * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)

Tactic:
simpa only [Nat.cast_mul, ofReal_natCast]
      using mul_cpow_ofReal_nonneg m.cast_nonneg n.cast_nonneg _

Premises used: Nat.cast_nonneg, Complex.mul_cpow_ofReal_nonneg, Nat.cast_mul, Complex.ofReal_natCast
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
n : ℕ
χ : DirichletCharacter ℂ n
hs : s ≠ 0
⊢ HMul.hMul (α := ℂ) ((χ : (a : ZMod n) → ℂ) (↑0 : ZMod n) : ℂ) (HPow.hPow (α := ℂ) (↑0 : ℂ) (-s)) = 0

Tactic:
simp [hs]
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
n : ℕ
χ : DirichletCharacter ℂ n
hs : s ≠ 0
⊢ HMul.hMul (α := ℂ) ((χ : (a : ZMod n) → ℂ) (↑1 : ZMod n) : ℂ) (HPow.hPow (α := ℂ) (↑1 : ℂ) (-s)) = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
n_1 : ℕ
χ : DirichletCharacter ℂ n_1
hs : s ≠ 0
m n : ℕ
⊢ HMul.hMul (α := ℂ) ((χ : (a : ZMod n_1) → ℂ) (↑(m * n) : ZMod n_1) : ℂ) ((↑(↑(m * n) : ℝ) : ℂ) ^ (-s)) =
    HMul.hMul (α := ℂ) ((χ : (a : ZMod n_1) → ℂ) (↑m : ZMod n_1) : ℂ) ((↑(↑m : ℝ) : ℂ) ^ (-s)) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod n_1) → ℂ) (↑n : ZMod n_1) : ℂ) ((↑(↑n : ℝ) : ℂ) ^ (-s))

Tactic:
simpa only [Nat.cast_mul, IsUnit.mul_iff, not_and, map_mul, ofReal_mul,
      mul_cpow_ofReal_nonneg m.cast_nonneg n.cast_nonneg _]
      using mul_mul_mul_comm ..

Premises used: IsUnit.mul_iff, mul_mul_mul_comm, Nat.cast_nonneg, Complex.mul_cpow_ofReal_nonneg, map_mul, Nat.cast_mul, not_and, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹

Tactic:
Real.summable_nat_rpow_inv.mpr hs

Premises used: Iff.mpr, Real.summable_nat_rpow_inv
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
h : ∀ (n : ℕ), ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖

Tactic:
convert! Real.summable_nat_rpow_inv.mpr hs with n

Premises used: Iff.mpr, Real.summable_nat_rpow_inv
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
h : ‖(↑(↑n : ℝ) : ℂ) ^ (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
h₁ : HPow.hPow (α := ℝ) (↑n : ℝ) (-s).re = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
h₂ : HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re) = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
h₃ h₄ : (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖ = (HPow.hPow (α := ℝ) (↑n : ℝ) s.re)⁻¹

Tactic:
rw [← ofReal_natCast,
    norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs,
    neg_re, Real.rpow_neg <| Nat.cast_nonneg n]

Premises used: Nat.cast_nonneg, Complex.neg_re, Complex.ofReal_natCast, Complex.norm_cpow_eq_rpow_re_of_nonneg, Complex.re_neg_ne_zero_of_one_lt_re, Real.rpow_neg
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := ℂ) ((riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n : ℂ)

Tactic:
have hsum := summable_riemannZetaSummand hs
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := ℂ) ((riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n : ℂ)
rw :
  Eq (α := ℂ) (∑' (b : ℕ), (riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) (b + 1))
    (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s)
⊢ ∑' (n : ℕ), (riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n = riemannZeta s

Tactic:
rw [zeta_eq_tsum_one_div_nat_add_one_cpow hs, hsum.of_norm.tsum_eq_zero_add, map_zero, zero_add]

Premises used: Summable.of_norm, Summable.tsum_eq_zero_add, map_zero, zero_add, zeta_eq_tsum_one_div_nat_add_one_cpow
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := ℂ) ((riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n : ℂ)
⊢ Eq (α := ℂ) (∑' (b : ℕ), (riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) (b + 1))
    (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s)

Tactic:
simp only [riemannZetaSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
    Nat.cast_add, Nat.cast_one, one_div]

Premises used: riemannZetaSummandHom, MonoidWithZeroHom.coe_mk, Complex.cpow_neg, ZeroHom.coe_mk, Nat.cast_add, one_div, Nat.cast_one
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
simp :
  Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := ℂ) ((dirichletSummandHom χ ⋯ : (a : ℕ) → ℂ) n : ℂ)

Tactic:
simp only [dirichletSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, norm_mul]

Premises used: MonoidWithZeroHom.coe_mk, norm_mul, dirichletSummandHom, ZeroHom.coe_mk
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
x : ℕ
⊢ 0 ≤ norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑x : ZMod N) : ℂ) * ‖HPow.hPow (α := ℂ) (↑x : ℂ) (-s)‖

Tactic:
positivity
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-s)‖

Tactic:
exact (summable_riemannZetaSummand hs).of_nonneg_of_le (fun _ ↦ by positivity)
    (fun n ↦ mul_le_of_le_one_left (norm_nonneg _) <| χ.norm_le_one n)
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ ∑' (n : ℕ), (dirichletSummandHom χ ⋯ : (a : ℕ) → ℂ) n = L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s

Tactic:
simp only [dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, LSeries,
    LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), div_eq_mul_inv]

Premises used: MonoidWithZeroHom.coe_mk, Complex.ne_zero_of_one_lt_re, Complex.cpow_neg, dirichletSummandHom, div_eq_mul_inv, LSeries, ZeroHom.coe_mk, LSeries.term_of_ne_zero'
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
rw :
  HasProd (α := ℂ) (fun (p : Primes) ↦ (1 - HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))⁻¹)
    (∑' (n : ℕ), (riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n)
⊢ HasProd (fun (p : Primes) ↦ (1 - HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))⁻¹) (riemannZeta s)

Tactic:
rw [← tsum_riemannZetaSummand hs]

Premises used: tsum_riemannZetaSummand
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
⊢ HasProd (α := ℂ) (fun (p : Primes) ↦ (1 - HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))⁻¹)
    (∑' (n : ℕ), (riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n)

Tactic:
apply eulerProduct_completely_multiplicative_hasProd <| summable_riemannZetaSummand hs

Premises used: summable_riemannZetaSummand, EulerProduct.eulerProduct_completely_multiplicative_hasProd
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
⊢ ∏' (p : Primes), (1 - HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))⁻¹ = riemannZeta s

Tactic:
(riemannZeta_eulerProduct_hasProd hs).tprod_eq

Premises used: HasProd.tprod_eq, riemannZeta_eulerProduct_hasProd
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
rw :
  Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))⁻¹) atTop
    (𝓝 (∑' (n : ℕ), (riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n))
⊢ Tendsto (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))⁻¹) atTop (𝓝 (riemannZeta s))

Tactic:
rw [← tsum_riemannZetaSummand hs]

Premises used: tsum_riemannZetaSummand
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, (1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s))⁻¹) atTop
    (𝓝 (∑' (n : ℕ), (riemannZetaSummandHom ⋯ : (a : ℕ) → ℂ) n))

Tactic:
apply eulerProduct_completely_multiplicative <| summable_riemannZetaSummand hs

Premises used: summable_riemannZetaSummand, EulerProduct.eulerProduct_completely_multiplicative
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
rw :
  HasProd (α := ℂ)
    (fun (p : Primes) ↦
      (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹)
    (∑' (n : ℕ), (dirichletSummandHom χ ⋯ : (a : ℕ) → ℂ) n)
⊢ HasProd
    (fun (p : Primes) ↦
      (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹)
    (L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s)

Tactic:
rw [← tsum_dirichletSummand χ hs]

Premises used: tsum_dirichletSummand
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd (α := ℂ)
    (fun (p : Primes) ↦ (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((dirichletSummandHom χ ⋯ : (a : ℕ) → ℂ) (↑p : ℕ) : ℂ))⁻¹)
    (∑' (n : ℕ), (dirichletSummandHom χ ⋯ : (a : ℕ) → ℂ) n)

Tactic:
eulerProduct_completely_multiplicative_hasProd <| summable_dirichletSummand χ hs

Premises used: EulerProduct.eulerProduct_completely_multiplicative_hasProd, summable_dirichletSummand
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd (α := ℂ)
    (fun (p : Primes) ↦
      (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹)
    (∑' (n : ℕ), (dirichletSummandHom χ ⋯ : (a : ℕ) → ℂ) n)

Tactic:
convert! eulerProduct_completely_multiplicative_hasProd <| summable_dirichletSummand χ hs

Premises used: EulerProduct.eulerProduct_completely_multiplicative_hasProd, summable_dirichletSummand
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ ∏' (p : Primes),
      (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))⁻¹ =
    L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s

Tactic:
(DirichletCharacter.LSeries_eulerProduct_hasProd χ hs).tprod_eq

Premises used: HasProd.tprod_eq, DirichletCharacter.LSeries_eulerProduct_hasProd
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
rw :
  Tendsto (β := ℂ)
    (fun (n : ℕ) ↦
      ∏ p ∈ n.primesBelow,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
    atTop (𝓝 (∑' (n : ℕ), (dirichletSummandHom χ ⋯ : (a : ℕ) → ℂ) n))
⊢ Tendsto
    (fun (n : ℕ) ↦
      ∏ p ∈ n.primesBelow,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
    atTop (𝓝 (L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s))

Tactic:
rw [← tsum_dirichletSummand χ hs]

Premises used: tsum_dirichletSummand
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Tendsto (β := ℂ)
    (fun (n : ℕ) ↦
      ∏ p ∈ n.primesBelow,
        (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹)
    atTop (𝓝 (∑' (n : ℕ), (dirichletSummandHom χ ⋯ : (a : ℕ) → ℂ) n))

Tactic:
apply eulerProduct_completely_multiplicative <| summable_dirichletSummand χ hs

Premises used: EulerProduct.eulerProduct_completely_multiplicative, summable_dirichletSummand
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
n : ℕ
inl : term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s 0 = (f : (a : ℕ) → ℂ) 0
inr : ∀ (hn : n ≠ 0), term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s n = (f : (a : ℕ) → ℂ) n
⊢ term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s n = (f : (a : ℕ) → ℂ) n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
⊢ term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s 0 = (f : (a : ℕ) → ℂ) 0

Tactic:
simp only [term_zero, map_zero]

Premises used: map_zero, LSeries.term_zero
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
n : ℕ
hn : n ≠ 0
⊢ term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s n = (f : (a : ℕ) → ℂ) n

Tactic:
simp only [ne_eq, hn, not_false_eq_true, term_of_ne_zero, div_eq_mul_inv,
        dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, f]

Premises used: MonoidWithZeroHom.coe_mk, LSeries.term_of_ne_zero, Complex.cpow_neg, dirichletSummandHom, ne_eq, div_eq_mul_inv, ZeroHom.coe_mk, not_false_eq_true
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
⊢ ∀ (n : ℕ), term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s n = (f : (a : ℕ) → ℂ) n

Tactic:
have h n : term ↗χ s n = f n := by
    rcases eq_or_ne n 0 with rfl | hn
    · simp only [term_zero, map_zero]
    · simp only [ne_eq, hn, not_false_eq_true, term_of_ne_zero, div_eq_mul_inv,
        dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, f]
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
h : ∀ (n : ℕ), term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s n = (f : (a : ℕ) → ℂ) n
⊢ cexp
      (∑' (p : Primes),
        -Complex.log
            (1 -
              HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
                (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))) =
    L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s

Tactic:
simpa only [LSeries, h]
    using exp_tsum_primes_log_eq_tsum (f := f) <| summable_dirichletSummand χ hs

Premises used: LSeries, summable_dirichletSummand, EulerProduct.exp_tsum_primes_log_eq_tsum
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
h :
  ∀ (x : Primes),
    HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) =
      HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑(↑x : ℕ) : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s))
⊢ cexp (∑' (p : Primes), -Complex.log (1 - HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))) = L 1 s

Tactic:
convert!
    modOne_eq_one (R := ℂ) ▸
      DirichletCharacter.LSeries_eulerProduct_exp_log (1 : DirichletCharacter ℂ 1) hs using 7
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
x : Primes
h : HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) = 1 * HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s)
h₁ h₂ : HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) = HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s)
⊢ HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s) =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod 1) → ℂ) (↑(↑x : ℕ) : ZMod 1) : ℂ) (HPow.hPow (α := ℂ) (↑(↑x : ℕ) : ℂ) (-s))

Tactic:
rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]

Premises used: MulChar.one_apply, isUnit_of_subsingleton, one_mul
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -Complex.log (1 - HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))) = riemannZeta s

Tactic:
LSeries_one_eq_riemannZeta hs ▸ ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log hs

Premises used: Eq.rec, LSeries_one_eq_riemannZeta, ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log