awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this : NeZero q
⊢ IsUnit (M := ZMod q) (↑a : ZMod q)

Tactic:
have : IsUnit (a : ZMod q) := by
    rwa [ZMod.coe_int_isUnit_iff_isCoprime, isCoprime_comm]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this_1 : NeZero q
this : IsUnit (M := ZMod q) (↑a : ZMod q)
obtain :
  ∀ (p : ℕ) (hpn : p > n) (hpp : Prime p) (heq : Eq (α := ZMod q) (↑p : ZMod q) (↑a : ZMod q)),
    ∃ p > n, Prime p ∧ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]
⊢ ∃ p > n, Prime p ∧ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]

Tactic:
obtain ⟨p, hpn, hpp, heq⟩ := forall_exists_prime_gt_and_eq_mod this n

Premises used: Nat.forall_exists_prime_gt_and_eq_mod
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this_1 : NeZero q
this : IsUnit (M := ZMod q) (↑a : ZMod q)
p : ℕ
hpn : p > n
hpp : Prime p
heq : Eq (α := ZMod q) (↑p : ZMod q) (↑a : ZMod q)
⊢ ∃ p > n, Prime p ∧ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]

Tactic:
⟨p, hpn, hpp, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this_1 : NeZero q
this : IsUnit (M := ZMod q) (↑a : ZMod q)
p : ℕ
hpn : p > n
hpp : Prime p
heq : Eq (α := ZMod q) (↑p : ZMod q) (↑a : ZMod q)
refine : (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]
⊢ ∃ p > n, Prime p ∧ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]

Tactic:
refine ⟨p, hpn, hpp, ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a (↑q : ℤ)
this_1 : NeZero q
this : IsUnit (M := ZMod q) (↑a : ZMod q)
p : ℕ
hpn : p > n
hpp : Prime p
heq : Eq (α := ZMod q) (↑p : ZMod q) (↑a : ZMod q)
⊢ (↑p : ℤ) ≡ a [ZMOD (↑q : ℤ)]

Tactic:
simpa [← ZMod.intCast_eq_intCast_iff] using heq

Premises used: ZMod.intCast_eq_intCast_iff
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
n q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ IsCoprime (R := ℤ) (↑a : ℤ) (↑q : ℤ)

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
n q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ ∃ p > n, Prime p ∧ p ≡ a [MOD q]

Tactic:
simpa using forall_exists_prime_gt_and_zmodEq n (q := q) (a := a) hq (by simpa)

Premises used: Nat.forall_exists_prime_gt_and_zmodEq
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q a : ℕ
hq : q ≠ 0
h : a.Coprime q
rw : ∀ (a_1 : ℕ), ∃ b ≥ a_1, Prime b ∧ b ≡ a [MOD q]
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ a [MOD q]

Tactic:
rw [frequently_atTop]

Premises used: Filter.frequently_atTop
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q a : ℕ
hq : q ≠ 0
h : a.Coprime q
n : ℕ
obtain : ∀ (p : ℕ) (hn : p > n) (hp : Prime p) (ha : p ≡ a [MOD q]), ∃ b ≥ n, Prime b ∧ b ≡ a [MOD q]
⊢ ∃ b ≥ n, Prime b ∧ b ≡ a [MOD q]

Tactic:
obtain ⟨p, hn, hp, ha⟩ := forall_exists_prime_gt_and_modEq n hq h

Premises used: Nat.forall_exists_prime_gt_and_modEq
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q a : ℕ
hq : q ≠ 0
h : a.Coprime q
n p : ℕ
hn : p > n
hp : Prime p
ha : p ≡ a [MOD q]
⊢ ∃ b ≥ n, Prime b ∧ b ≡ a [MOD q]

Tactic:
⟨p, hn.le, hp, ha⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q a : ℕ
hq : q ≠ 0
h : a.Coprime q
n p : ℕ
hn : p > n
hp : Prime p
ha : p ≡ a [MOD q]
⊢ ∃ b ≥ n, Prime b ∧ b ≡ a [MOD q]

Tactic:
exact ⟨p, hn.le, hp, ha⟩
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ Set.Infinite (α := ℕ) {p : ℕ | Prime p ∧ p ≡ a [MOD q]}

Tactic:
frequently_atTop_iff_infinite.1 (frequently_atTop_prime_and_modEq hq h)

Premises used: Nat.frequently_atTop_iff_infinite, Nat.frequently_atTop_prime_and_modEq, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
⊢ completedHurwitzZetaEven 0 s = completedRiemannZeta s

Tactic:
rfl

Premises used: completedRiemannZeta, rfl
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
⊢ completedHurwitzZetaEven₀ 0 s = completedRiemannZeta₀ s

Tactic:
rfl

Premises used: completedRiemannZeta₀, rfl
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
rw : completedCosZeta 0 s = completedHurwitzZetaEven 0 s
rw₁ : completedCosZeta 0 s = (hurwitzEvenFEPair 0).Λ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair 0).symm.Λ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ (s / 2) / 2
rw₃ rw₄ : (hurwitzEvenFEPair 0).Λ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ (s / 2) / 2
⊢ completedCosZeta 0 s = completedRiemannZeta s

Tactic:
rw [completedRiemannZeta, completedHurwitzZetaEven, completedCosZeta, hurwitzEvenFEPair_zero_symm]

Premises used: HurwitzZeta.hurwitzEvenFEPair_zero_symm, HurwitzZeta.completedHurwitzZetaEven, completedRiemannZeta, HurwitzZeta.completedCosZeta
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
rw : completedCosZeta₀ 0 s = completedHurwitzZetaEven₀ 0 s
rw₁ : completedCosZeta₀ 0 s = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair 0).symm.Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
rw₃ rw₄ : (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
⊢ completedCosZeta₀ 0 s = completedRiemannZeta₀ s

Tactic:
rw [completedRiemannZeta₀, completedHurwitzZetaEven₀, completedCosZeta₀,
    hurwitzEvenFEPair_zero_symm]

Premises used: HurwitzZeta.completedHurwitzZetaEven₀, HurwitzZeta.hurwitzEvenFEPair_zero_symm, HurwitzZeta.completedCosZeta₀, completedRiemannZeta₀
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
simp_rw : completedHurwitzZetaEven 0 s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)
simp_rw₁ : completedHurwitzZetaEven 0 s = completedHurwitzZetaEven₀ 0 s - 1 / s - 1 / (1 - s)
simp_rw₂ :
  completedHurwitzZetaEven₀ 0 s - (if True then 1 else 0) / s - 1 / (1 - s) =
    completedHurwitzZetaEven₀ 0 s - 1 / s - 1 / (1 - s)
⊢ completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)

Tactic:
simp_rw [completedRiemannZeta, completedRiemannZeta₀, completedHurwitzZetaEven_eq, if_true]

Premises used: if_true, HurwitzZeta.completedHurwitzZetaEven_eq, completedRiemannZeta₀, completedRiemannZeta
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ Differentiable ℂ completedRiemannZeta₀

Tactic:
differentiable_completedHurwitzZetaEven₀ 0

Premises used: completedRiemannZeta₀, OfNat.ofNat, HurwitzZeta.differentiable_completedHurwitzZetaEven₀
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ completedRiemannZeta s

Tactic:
differentiableAt_completedHurwitzZetaEven 0 (Or.inl hs) hs'

Premises used: HurwitzZeta.differentiableAt_completedHurwitzZetaEven, Or.inl, OfNat.ofNat, completedRiemannZeta
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
rw : completedHurwitzZetaEven₀ 0 (1 - s) = completedRiemannZeta₀ s
rw₁ : completedHurwitzZetaEven₀ 0 (1 - s) = completedCosZeta₀ 0 s
rw₂ rw₃ : completedCosZeta₀ 0 s = completedCosZeta₀ 0 s
⊢ completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s

Tactic:
rw [← completedHurwitzZetaEven₀_zero, ← completedCosZeta₀_zero, completedHurwitzZetaEven₀_one_sub]

Premises used: HurwitzZeta.completedCosZeta₀_zero, HurwitzZeta.completedHurwitzZetaEven₀_zero, HurwitzZeta.completedHurwitzZetaEven₀_one_sub
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
rw : completedHurwitzZetaEven 0 (1 - s) = completedRiemannZeta s
rw₁ : completedHurwitzZetaEven 0 (1 - s) = completedCosZeta 0 s
rw₂ rw₃ : completedCosZeta 0 s = completedCosZeta 0 s
⊢ completedRiemannZeta (1 - s) = completedRiemannZeta s

Tactic:
rw [← completedHurwitzZetaEven_zero, ← completedCosZeta_zero, completedHurwitzZetaEven_one_sub]

Premises used: HurwitzZeta.completedHurwitzZetaEven_one_sub, HurwitzZeta.completedHurwitzZetaEven_zero, HurwitzZeta.completedCosZeta_zero
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedRiemannZeta s) (𝓝[≠] 1) (𝓝 1)

Tactic:
completedHurwitzZetaEven_residue_one 0

Premises used: HurwitzZeta.completedHurwitzZetaEven_residue_one, OfNat.ofNat, completedRiemannZeta
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ hurwitzZetaEven 0 = riemannZeta

Tactic:
rfl

Premises used: riemannZeta, rfl
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
simp_rw :
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2) = riemannZeta
simp_rw₁ :
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2) = hurwitzZetaEven 0
simp_rw₂ :
  Eq (α := (a : ℂ) → ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2))
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven 0 s / s.Gammaℝ) 0
      (if True then -1 / 2 else 0))
simp_rw₃ :
  Eq (α := (a : ℂ) → ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2))
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven 0 s / s.Gammaℝ) 0 (-1 / 2))
simp_rw₄ :
  Eq (α := (a : ℂ) → ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2))
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedRiemannZeta s / s.Gammaℝ) 0 (-1 / 2))
⊢ cosZeta 0 = riemannZeta

Tactic:
simp_rw [cosZeta, riemannZeta, hurwitzZetaEven, if_true, completedHurwitzZetaEven_zero,
    completedCosZeta_zero]

Premises used: riemannZeta, if_true, HurwitzZeta.cosZeta, HurwitzZeta.completedHurwitzZetaEven_zero, HurwitzZeta.completedCosZeta_zero, HurwitzZeta.hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
h : ∀ (s : ℂ), hurwitzZeta 0 s = riemannZeta s
⊢ hurwitzZeta 0 = riemannZeta

Tactic:
ext1 s
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
⊢ hurwitzZeta 0 s = riemannZeta s

Tactic:
simpa [hurwitzZeta, hurwitzZetaEven_zero] using hurwitzZetaOdd_neg 0 s

Premises used: HurwitzZeta.hurwitzZetaEven_zero, HurwitzZeta.hurwitzZeta, HurwitzZeta.hurwitzZetaOdd_neg, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
h : ∀ (s : ℂ), expZeta 0 s = riemannZeta s
⊢ expZeta 0 = riemannZeta

Tactic:
ext1 s
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
h : cosZeta 0 s + I * sinZeta 0 s = riemannZeta s
h₁ : riemannZeta s + I * sinZeta 0 s = riemannZeta s
h₂ : I * sinZeta 0 s = 0
h₃ : I = 0 ∨ sinZeta 0 s = 0
h₄ : False ∨ sinZeta 0 s = 0
h₅ : sinZeta 0 s = 0
h₆ : sinZeta 0 s = -sinZeta 0 s
h₇ : sinZeta 0 s = sinZeta (-0) s
h₈ h₉ : sinZeta 0 s = sinZeta 0 s
⊢ expZeta 0 s = riemannZeta s

Tactic:
rw [expZeta, cosZeta_zero, add_eq_left, mul_eq_zero, eq_false_intro I_ne_zero, false_or,
    ← eq_neg_self_iff, ← sinZeta_neg, neg_zero]

Premises used: Complex.I_ne_zero, false_or, mul_eq_zero, CharZero.eq_neg_self_iff, HurwitzZeta.expZeta, HurwitzZeta.cosZeta_zero, add_eq_left, HurwitzZeta.sinZeta_neg, neg_zero, eq_false_intro
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ riemannZeta s

Tactic:
differentiableAt_hurwitzZetaEven _ hs'

Premises used: HurwitzZeta.differentiableAt_hurwitzZetaEven, riemannZeta
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ DifferentiableOn ℂ riemannZeta {1}ᶜ

Tactic:
fun _ hs ↦ (differentiableAt_riemannZeta hs).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_riemannZeta, DifferentiableOn
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ AnalyticOnNhd ℂ riemannZeta {1}ᶜ

Tactic:
differentiableOn_riemannZeta.analyticOnNhd isOpen_compl_singleton

Premises used: isOpen_compl_singleton, differentiableOn_riemannZeta, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
simp_rw : hurwitzZetaEven 0 0 = -1 / 2
simp_rw₁ :
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven 0 s / s.Gammaℝ) 0
      (if True then -1 / 2 else 0) 0 =
    -1 / 2
simp_rw₂ : (if True then -1 / 2 else 0) = -1 / 2
⊢ riemannZeta 0 = -1 / 2

Tactic:
simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, if_true]

Premises used: riemannZeta, if_true, Function.update_self, HurwitzZeta.hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : s ≠ 0
rw : hurwitzZetaEven 0 s = completedRiemannZeta s / s.Gammaℝ
rw₁ :
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven 0 s / s.Gammaℝ) 0
      (if Eq (α := UnitAddCircle) 0 0 then -1 / 2 else 0) s =
    completedRiemannZeta s / s.Gammaℝ
rw₂ : completedHurwitzZetaEven 0 s / s.Gammaℝ = completedRiemannZeta s / s.Gammaℝ
rw₃ rw₄ : completedRiemannZeta s / s.Gammaℝ = completedRiemannZeta s / s.Gammaℝ
⊢ riemannZeta s = completedRiemannZeta s / s.Gammaℝ

Tactic:
rw [riemannZeta, hurwitzZetaEven, Function.update_of_ne hs, completedHurwitzZetaEven_zero]

Premises used: riemannZeta, HurwitzZeta.completedHurwitzZetaEven_zero, HurwitzZeta.hurwitzZetaEven, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
n : ℕ
⊢ riemannZeta (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0

Tactic:
hurwitzZetaEven_neg_two_mul_nat_add_one 0 n

Premises used: riemannZeta, HurwitzZeta.hurwitzZetaEven_neg_two_mul_nat_add_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : s ≠ 1
rw : hurwitzZetaEven 0 (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * hurwitzZetaEven 0 s
rw₁ :
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * cosZeta 0 s =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * hurwitzZetaEven 0 s
rw₂ :
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta s =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * hurwitzZetaEven 0 s
rw₃ rw₄ :
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta s =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta s
⊢ riemannZeta (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta s

Tactic:
rw [riemannZeta, hurwitzZetaEven_one_sub 0 hs (Or.inr hs'), cosZeta_zero, hurwitzZetaEven_zero]

Premises used: riemannZeta, HurwitzZeta.hurwitzZetaEven_zero, HurwitzZeta.hurwitzZetaEven_one_sub, HurwitzZeta.cosZeta_zero, OfNat.ofNat, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
⊢ completedCosZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * 0 * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s

Tactic:
have := (hasSum_nat_completedCosZeta 0 hs).tsum_eq.symm
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
this :
  completedCosZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * 0 * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s
⊢ completedRiemannZeta s =
    ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * 0 * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s

Tactic:
simp only [QuotientAddGroup.mk_zero, completedCosZeta_zero] at this

Premises used: QuotientAddGroup.mk_zero, HurwitzZeta.completedCosZeta_zero
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
this :
  completedRiemannZeta s =
    ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * 0 * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s
simp :
  Eq (α := ℂ) (∑' (b : ℕ), if b = 0 then 0 else (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑b : ℂ) s)
    (∑' (x : ℕ), (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑x : ℂ) s)
⊢ completedRiemannZeta s = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
simp only [this, Gammaℝ_def, mul_zero, zero_mul, Real.cos_zero, ofReal_one, mul_one, mul_one_div,
    ← tsum_mul_left]

Premises used: Complex.Gammaℝ_def, MulZeroClass.zero_mul, tsum_mul_left, Complex.ofReal_one, MulZeroClass.mul_zero, mul_one_div, mul_one, Real.cos_zero
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
this :
  completedRiemannZeta s =
    ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * 0 * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s
e_f :
  ∀ (n : ℕ),
    (if n = 0 then 0 else (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s) =
      (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ Eq (α := ℂ) (∑' (b : ℕ), if b = 0 then 0 else (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑b : ℂ) s)
    (∑' (x : ℕ), (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑x : ℂ) s)

Tactic:
congr 1 with n
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
this :
  completedRiemannZeta s =
    ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * 0 * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s
n : ℕ
pos : ∀ (h : n = 0), 0 = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s
neg :
  ∀ (h : ¬n = 0),
    (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
      (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (if n = 0 then 0 else (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s) =
    (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
this :
  completedRiemannZeta s =
    ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * 0 * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s
n : ℕ
h : n = 0
⊢ 0 = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
simp only [h, Nat.cast_zero, zero_cpow (Complex.ne_zero_of_one_lt_re hs), div_zero]

Premises used: Complex.ne_zero_of_one_lt_re, Complex.zero_cpow, Nat.cast_zero, div_zero
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
this :
  completedRiemannZeta s =
    ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * 0 * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s
n : ℕ
h : ¬n = 0
⊢ (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
⊢ riemannZeta s = ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
simpa only [QuotientAddGroup.mk_zero, cosZeta_zero, mul_zero, zero_mul, Real.cos_zero,
    ofReal_one] using (hasSum_nat_cosZeta 0 hs).tsum_eq.symm

Premises used: MulZeroClass.zero_mul, HurwitzZeta.hasSum_nat_cosZeta, Complex.ofReal_one, MulZeroClass.mul_zero, HurwitzZeta.cosZeta_zero, HasSum.tsum_eq, QuotientAddGroup.mk_zero, OfNat.ofNat, Eq.symm, Real.cos_zero
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
⊢ riemannZeta s = ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
have := zeta_eq_tsum_one_div_nat_cpow hs
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
rw :
  ∀ (this : riemannZeta s = 1 / HPow.hPow (α := ℂ) (↑0 : ℂ) s + ∑' (b : ℕ), 1 / HPow.hPow (α := ℂ) (↑(b + 1) : ℂ) s),
    riemannZeta s = ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s
rw₁ : Summable (α := ℂ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ riemannZeta s = ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s

Tactic:
rw [Summable.tsum_eq_zero_add] at this

Premises used: Summable.tsum_eq_zero_add
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = 1 / HPow.hPow (α := ℂ) (↑0 : ℂ) s + ∑' (b : ℕ), 1 / HPow.hPow (α := ℂ) (↑(b + 1) : ℂ) s
⊢ riemannZeta s = ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s

Tactic:
simpa [zero_cpow (Complex.ne_zero_of_one_lt_re hs)]

Premises used: Complex.ne_zero_of_one_lt_re, Complex.zero_cpow
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
rwa rwa₁ rwa₂ rwa₃ : 1 < s.re
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rwa [Complex.summable_one_div_nat_cpow]

Premises used: Complex.summable_one_div_nat_cpow
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 1 < k
rwa : 1 < (↑(↑k : ℝ) : ℂ).re
rwa₁ : LT.lt (α := ℝ) 1 (↑k : ℝ)
rwa₂ : LT.lt (α := ℝ) (↑1 : ℝ) (↑k : ℝ)
rwa₃ rwa₄ rwa₅ rwa₆ : 1 < k
⊢ 1 < re (↑k : ℂ)

Tactic:
rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt]

Premises used: Complex.ofReal_natCast, Complex.ofReal_re, Nat.cast_lt, Nat.cast_one
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 1 < k
⊢ riemannZeta (↑k : ℂ) = ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) k

Tactic:
simp only [zeta_eq_tsum_one_div_nat_cpow
      (by rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt] : 1 < re k),
    cpow_natCast]

Premises used: zeta_eq_tsum_one_div_nat_cpow, Complex.cpow_natCast
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
linarith : k ≤ 1 → -1 + HSub.hSub (α := ℤ) 2 (↑k : ℤ) + HSub.hSub (α := ℤ) (↑k : ℤ) 1 = 0
⊢ 1 < k

Tactic:
linarith
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
⊢ 1 < k

Tactic:
have hkk : 1 < k := by linarith
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
rw :
  2 * riemannZeta (↑k : ℂ) =
    (HPow.hPow (α := ℂ) (↑0 : ℂ) k)⁻¹ +
      HSMul.hSMul (α := ℕ) (β := ℂ) 2 (∑' (n : ℕ+), (HPow.hPow (α := ℂ) (↑(↑(↑n : ℕ) : ℤ) : ℂ) k)⁻¹)
hf : Function.Even (β := ℂ) fun (n : ℤ) ↦ (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹
hf2 : Summable (α := ℂ) fun (n : ℤ) ↦ (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹
⊢ 2 * riemannZeta (↑k : ℂ) = ∑' (n : ℤ), (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹

Tactic:
rw [tsum_int_eq_zero_add_two_mul_tsum_pnat]

Premises used: tsum_int_eq_zero_add_two_mul_tsum_pnat
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
simp : ¬k = 0
⊢ (HPow.hPow (α := ℂ) 0 k)⁻¹ = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ ¬k = 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ (HPow.hPow (α := ℂ) 0 k)⁻¹ = 0

Tactic:
have h0 : (0 ^ k : ℂ)⁻¹ = 0 := by simp; lia
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
h0 : (HPow.hPow (α := ℂ) 0 k)⁻¹ = 0
norm_cast :
  2 * riemannZeta (↑k : ℂ) =
    (↑(HPow.hPow (α := ℕ) 0 k) : ℂ)⁻¹ + HSMul.hSMul (α := ℕ) (β := ℂ) 2 (∑' (n : ℕ+), (↑(↑(n ^ k) : ℕ) : ℂ)⁻¹)
⊢ 2 * riemannZeta (↑k : ℂ) =
    (HPow.hPow (α := ℂ) (↑0 : ℂ) k)⁻¹ +
      HSMul.hSMul (α := ℕ) (β := ℂ) 2 (∑' (n : ℕ+), (HPow.hPow (α := ℂ) (↑(↑(↑n : ℕ) : ℤ) : ℂ) k)⁻¹)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
h0 : (HPow.hPow (α := ℂ) 0 k)⁻¹ = 0
⊢ 1 < re (↑k : ℂ)

Tactic:
simp [hkk]
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
h0 : (HPow.hPow (α := ℂ) 0 k)⁻¹ = 0
⊢ 2 * riemannZeta (↑k : ℂ) =
    (↑(HPow.hPow (α := ℕ) 0 k) : ℂ)⁻¹ + HSMul.hSMul (α := ℕ) (β := ℂ) 2 (∑' (n : ℕ+), (↑(↑(n ^ k) : ℕ) : ℂ)⁻¹)

Tactic:
simp [h0, zeta_eq_tsum_one_div_nat_add_one_cpow (s := k) (by simp [hkk]),
      tsum_pnat_eq_tsum_succ (f := fun n => ((n : ℂ) ^ k)⁻¹)]

Premises used: tsum_pnat_eq_tsum_succ, zeta_eq_tsum_one_div_nat_add_one_cpow
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
n : ℤ
⊢ Eq (α := ℂ) ((fun (n : ℤ) ↦ (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹) (-n))
    ((fun (n : ℤ) ↦ (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹) n)

Tactic:
simp [Even.neg_pow hk2]

Premises used: Even.neg_pow
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)⁻¹‖

Tactic:
simp [hkk]
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(HPow.hPow (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) k)⁻¹‖

Tactic:
simp [hkk]