awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedHurwitzZetaEven 0 (1 - s) = completedRiemannZeta s
⊢ completedRiemannZeta (1 - s) = completedRiemannZeta s
have rw₁ : completedHurwitzZetaEven 0 (1 - s) = completedCosZeta 0 s
Tactic: rw [← completedHurwitzZetaEven_zero, ← completedCosZeta_zero, completedHurwitzZetaEven_one_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
rw : completedHurwitzZetaEven 0 (1 - s) = completedRiemannZeta s
rw₁ : completedHurwitzZetaEven 0 (1 - s) = completedCosZeta 0 s
⊢ completedRiemannZeta (1 - s) = completedRiemannZeta s
have rw₂ : completedCosZeta 0 s = completedCosZeta 0 s
Tactic: rw [← completedHurwitzZetaEven_zero, ← completedCosZeta_zero, completedHurwitzZetaEven_one_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
⊢ cosZeta 0 = riemannZeta
have simp_rw : Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2) = riemannZeta
Tactic: simp_rw [cosZeta, riemannZeta, hurwitzZetaEven, if_true, completedHurwitzZetaEven_zero,
    completedCosZeta_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
simp_rw :
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2) = riemannZeta
⊢ cosZeta 0 = riemannZeta
have simp_rw₁ : Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2) = hurwitzZetaEven 0
Tactic: simp_rw [cosZeta, riemannZeta, hurwitzZetaEven, if_true, completedHurwitzZetaEven_zero,
    completedCosZeta_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ cosZeta 0 = riemannZeta
have 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))
Tactic: simp_rw [cosZeta, riemannZeta, hurwitzZetaEven, if_true, completedHurwitzZetaEven_zero,
    completedCosZeta_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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))
⊢ cosZeta 0 = riemannZeta
have 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))
Tactic: simp_rw [cosZeta, riemannZeta, hurwitzZetaEven, if_true, completedHurwitzZetaEven_zero,
    completedCosZeta_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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))
⊢ cosZeta 0 = riemannZeta
have 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))
Tactic: simp_rw [cosZeta, riemannZeta, hurwitzZetaEven, if_true, completedHurwitzZetaEven_zero,
    completedCosZeta_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
⊢ hurwitzZeta 0 = riemannZeta
have h : ∀ (s : ℂ), hurwitzZeta 0 s = riemannZeta s
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
⊢ expZeta 0 = riemannZeta
have h : ∀ (s : ℂ), expZeta 0 s = riemannZeta s
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
⊢ expZeta 0 s = riemannZeta s
have h : cosZeta 0 s + I * sinZeta 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
h : cosZeta 0 s + I * sinZeta 0 s = riemannZeta s
⊢ expZeta 0 s = riemannZeta s
have h₁ : riemannZeta s + I * sinZeta 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
h : cosZeta 0 s + I * sinZeta 0 s = riemannZeta s
h₁ : riemannZeta s + I * sinZeta 0 s = riemannZeta s
⊢ expZeta 0 s = riemannZeta s
have h₂ : I * sinZeta 0 s = 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ expZeta 0 s = riemannZeta s
have h₃ : I = 0 ∨ sinZeta 0 s = 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ expZeta 0 s = riemannZeta s
have h₄ : False ∨ sinZeta 0 s = 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ expZeta 0 s = riemannZeta s
have h₅ : sinZeta 0 s = 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ expZeta 0 s = riemannZeta s
have h₆ : sinZeta 0 s = -sinZeta 0 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ expZeta 0 s = riemannZeta s
have h₇ : sinZeta 0 s = sinZeta (-0) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ expZeta 0 s = riemannZeta s
have h₈ : sinZeta 0 s = sinZeta 0 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
⊢ riemannZeta 0 = -1 / 2
have simp_rw : hurwitzZetaEven 0 0 = -1 / 2
Tactic: simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, if_true]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
simp_rw : hurwitzZetaEven 0 0 = -1 / 2
⊢ riemannZeta 0 = -1 / 2
have simp_rw₁ : Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven 0 s / s.Gammaℝ) 0
    (if True then -1 / 2 else 0) 0 =
  -1 / 2
Tactic: simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, if_true]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ riemannZeta 0 = -1 / 2
have simp_rw₂ : (if True then -1 / 2 else 0) = -1 / 2
Tactic: simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, if_true]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
hs : s ≠ 0
⊢ riemannZeta s = completedRiemannZeta s / s.Gammaℝ
have rw : hurwitzZetaEven 0 s = completedRiemannZeta s / s.Gammaℝ
Tactic: rw [riemannZeta, hurwitzZetaEven, Function.update_of_ne hs, completedHurwitzZetaEven_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
hs : s ≠ 0
rw : hurwitzZetaEven 0 s = completedRiemannZeta s / s.Gammaℝ
⊢ riemannZeta s = completedRiemannZeta s / s.Gammaℝ
have 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ℝ
Tactic: rw [riemannZeta, hurwitzZetaEven, Function.update_of_ne hs, completedHurwitzZetaEven_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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ℝ
⊢ riemannZeta s = completedRiemannZeta s / s.Gammaℝ
have rw₂ : completedHurwitzZetaEven 0 s / s.Gammaℝ = completedRiemannZeta s / s.Gammaℝ
Tactic: rw [riemannZeta, hurwitzZetaEven, Function.update_of_ne hs, completedHurwitzZetaEven_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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ℝ
⊢ riemannZeta s = completedRiemannZeta s / s.Gammaℝ
have rw₃ : completedRiemannZeta s / s.Gammaℝ = completedRiemannZeta s / s.Gammaℝ
Tactic: rw [riemannZeta, hurwitzZetaEven, Function.update_of_ne hs, completedHurwitzZetaEven_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : s ≠ 1
⊢ riemannZeta (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta s
have rw : hurwitzZetaEven 0 (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * hurwitzZetaEven 0 s
Tactic: rw [riemannZeta, hurwitzZetaEven_one_sub 0 hs (Or.inr hs'), cosZeta_zero, hurwitzZetaEven_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ riemannZeta (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta s
have rw₁ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * cosZeta 0 s =
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * hurwitzZetaEven 0 s
Tactic: rw [riemannZeta, hurwitzZetaEven_one_sub 0 hs (Or.inr hs'), cosZeta_zero, hurwitzZetaEven_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ riemannZeta (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta s
have rw₂ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta s =
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * hurwitzZetaEven 0 s
Tactic: rw [riemannZeta, hurwitzZetaEven_one_sub 0 hs (Or.inr hs'), cosZeta_zero, hurwitzZetaEven_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ riemannZeta (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta s
have rw₃ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) * riemannZeta 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (hypothesis)
Goal:
s : ℂ
hs : 1 < s.re
⊢ completedRiemannZeta s = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
have 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
Tactic: have := (hasSum_nat_completedCosZeta 0 hs).tsum_eq.symm
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (hypothesis)
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 = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ completedRiemannZeta s = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
have 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)
Tactic: simp only [this, Gammaℝ_def, mul_zero, zero_mul, Real.cos_zero, ofReal_one, mul_one, mul_one_div,
    ← tsum_mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ 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)
have 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
Tactic: congr 1 with n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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 : ℕ
⊢ (if n = 0 then 0 else (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s) =
    (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s
have pos : ∀ (h : n = 0), 0 = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ (if n = 0 then 0 else (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s) =
    (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s
have neg : ∀ (h : ¬n = 0),
  (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (hypothesis)
Goal:
s : ℂ
hs : 1 < s.re
⊢ riemannZeta s = ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s
have this : riemannZeta s = ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: have := zeta_eq_tsum_one_div_nat_cpow hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ riemannZeta s = ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s
have 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
Tactic: rw [Summable.tsum_eq_zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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
⊢ riemannZeta s = ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ s
have rw₁ : Summable (α := ℂ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [Summable.tsum_eq_zero_add] at this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
k : ℕ
hk : 1 < k
⊢ 1 < re (↑k : ℂ)
have rwa : 1 < (↑(↑k : ℝ) : ℂ).re
Tactic: rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
k : ℕ
hk : 1 < k
rwa : 1 < (↑(↑k : ℝ) : ℂ).re
⊢ 1 < re (↑k : ℂ)
have rwa₁ : LT.lt (α := ℝ) 1 (↑k : ℝ)
Tactic: rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
k : ℕ
hk : 1 < k
rwa : 1 < (↑(↑k : ℝ) : ℂ).re
rwa₁ : LT.lt (α := ℝ) 1 (↑k : ℝ)
⊢ 1 < re (↑k : ℂ)
have rwa₂ : LT.lt (α := ℝ) (↑1 : ℝ) (↑k : ℝ)
Tactic: rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
⊢ 1 < k
have linarith : k ≤ 1 → -1 + HSub.hSub (α := ℤ) 2 (↑k : ℤ) + HSub.hSub (α := ℤ) (↑k : ℤ) 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (hypothesis)
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
⊢ 2 * riemannZeta (↑k : ℂ) = ∑' (n : ℤ), (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹
have hkk : 1 < k
Tactic: have hkk : 1 < k := by linarith
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ 2 * riemannZeta (↑k : ℂ) = ∑' (n : ℤ), (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹
have rw : 2 * riemannZeta (↑k : ℂ) =
  (HPow.hPow (α := ℂ) (↑0 : ℂ) k)⁻¹ +
    HSMul.hSMul (α := ℕ) (β := ℂ) 2 (∑' (n : ℕ+), (HPow.hPow (α := ℂ) (↑(↑(↑n : ℕ) : ℤ) : ℂ) k)⁻¹)
Tactic: rw [tsum_int_eq_zero_add_two_mul_tsum_pnat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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)⁻¹)
⊢ 2 * riemannZeta (↑k : ℂ) = ∑' (n : ℤ), (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹
have hf : Function.Even (β := ℂ) fun (n : ℤ) ↦ (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹
Tactic: rw [tsum_int_eq_zero_add_two_mul_tsum_pnat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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)⁻¹
⊢ 2 * riemannZeta (↑k : ℂ) = ∑' (n : ℤ), (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹
have hf2 : Summable (α := ℂ) fun (n : ℤ) ↦ (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹
Tactic: rw [tsum_int_eq_zero_add_two_mul_tsum_pnat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ (HPow.hPow (α := ℂ) 0 k)⁻¹ = 0
have simp : ¬k = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (hypothesis)
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ 2 * riemannZeta (↑k : ℂ) =
    (HPow.hPow (α := ℂ) (↑0 : ℂ) k)⁻¹ +
      HSMul.hSMul (α := ℕ) (β := ℂ) 2 (∑' (n : ℕ+), (HPow.hPow (α := ℂ) (↑(↑(↑n : ℕ) : ℤ) : ℂ) k)⁻¹)
have h0 : (HPow.hPow (α := ℂ) 0 k)⁻¹ = 0
Tactic: have h0 : (0 ^ k : ℂ)⁻¹ = 0 := by simp; lia
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
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 : ℕ+), (HPow.hPow (α := ℂ) (↑(↑(↑n : ℕ) : ℤ) : ℂ) k)⁻¹)
have norm_cast : 2 * riemannZeta (↑k : ℂ) =
  (↑(HPow.hPow (α := ℕ) 0 k) : ℂ)⁻¹ + HSMul.hSMul (α := ℕ) (β := ℂ) 2 (∑' (n : ℕ+), (↑(↑(n ^ k) : ℕ) : ℂ)⁻¹)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s) (𝓝[{s : ℂ | 1 < s.re}] 1)
    (𝓝 1)
have refine_1 : Subset (α := Set ℂ) {s : ℂ | 1 < s.re} {1}ᶜ
Tactic: refine (tendsto_nhdsWithin_mono_left ?_ riemannZeta_residue_one).congr' ?_