awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
e_a : -(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) = -(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
⊢ I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) -
      I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) =
    I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) -
      I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
have e_a₁ : 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I = 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)
Tactic: congr 3
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
b : ℝ
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
have H : ∀ (p : ℝ) (hp : 0 < p)
  (hp' :
    IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦
      rexp (-p * t)),
  ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
Tactic: obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_one b
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
b p : ℝ
hp : 0 < p
hp' :
  IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
have H : ∀ᶠ (x : ℝ) in atTop,
  ‖oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x‖ ≤ HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x
Tactic: refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
b p : ℝ
hp : 0 < p
hp' :
  IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ‖oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x‖ ≤
      HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x
have h : ∀ (t : ℝ) (ht : 0 < t),
  ‖oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t‖ ≤ HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel a) fun (x : ℝ) ↦ rexp (-p * x)
have H : ∀ (b : ℝ),
  ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
Tactic: induction a using QuotientAddGroup.induction_on with | H b =>
  obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_one b
  refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
  filter_upwards [eventually_gt_atTop 0] with t ht
  simpa [← (hasSum_int_oddKernel b ht).tsum_eq, HurwitzKernelBounds.F_int,
    HurwitzKernelBounds.f_int, abs_of_nonneg (exp_pos _).le] using
    norm_tsum_le_tsum_norm (hasSum_int_oddKernel b ht).summable.norm
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
have H : ∀ (p : ℝ) (hp : 0 < p) (hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)),
  ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
Tactic: obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_one (le_refl 0)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
have H : ∀ᶠ (x : ℝ) in atTop, ‖sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 x
Tactic: refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 x
have h : ∀ (t : ℝ) (ht : 0 < t), ‖sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 t
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 t
have h : Norm.norm (E := ℝ)
    (∑' (b : ℕ),
      HMul.hMul (α := ℝ) 2 (↑b : ℝ) * Real.sin (2 * π * a * (↑b : ℝ)) *
        rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2 * t)) ≤
  HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n)
Tactic: rw [HurwitzKernelBounds.F_nat, ← (hasSum_nat_sinKernel a ht).tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ Norm.norm (E := ℝ)
      (∑' (b : ℕ),
        HMul.hMul (α := ℝ) 2 (↑b : ℝ) * Real.sin (2 * π * a * (↑b : ℝ)) *
          rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2 * t)) ≤
    HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n)
have h : HasSum (fun (n : ℕ) ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)
  (HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n))
Tactic: apply tsum_of_norm_bounded (g := fun n ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
h :
  HasSum (fun (n : ℕ) ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)
    (HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n))
⊢ Norm.norm (E := ℝ)
      (∑' (b : ℕ),
        HMul.hMul (α := ℝ) 2 (↑b : ℝ) * Real.sin (2 * π * a * (↑b : ℝ)) *
          rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2 * t)) ≤
    HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n)
have h₁ : ∀ (i : ℕ),
  ‖HMul.hMul (α := ℝ) 2 (↑i : ℝ) * Real.sin (2 * π * a * (↑i : ℝ)) *
        rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 * t)‖ ≤
    2 * HurwitzKernelBounds.f_nat 1 0 t i
Tactic: apply tsum_of_norm_bounded (g := fun n ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖HMul.hMul (α := ℝ) 2 (↑n : ℝ) * Real.sin (2 * π * a * (↑n : ℝ)) *
        rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)‖ ≤
    2 * HurwitzKernelBounds.f_nat 1 0 t n
have h : (↑n : ℝ) * ‖Real.sin (2 * π * a * (↑n : ℝ))‖ ≤ (↑n : ℝ)
Tactic: rw [norm_mul, norm_mul, norm_mul, norm_two, mul_assoc, mul_assoc,
      mul_le_mul_iff_of_pos_left two_pos, HurwitzKernelBounds.f_nat, pow_one, add_zero,
      norm_of_nonneg (exp_pos _).le, Real.norm_eq_abs, Nat.abs_cast, ← mul_assoc,
      mul_le_mul_iff_of_pos_right (exp_pos _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel a) fun (x : ℝ) ↦ rexp (-p * x)
have H : ∀ (a : ℝ),
  ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
Tactic: induction a using QuotientAddGroup.induction_on with | H a =>
  obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_one (le_refl 0)
  refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
  filter_upwards [eventually_gt_atTop 0] with t ht
  rw [HurwitzKernelBounds.F_nat, ← (hasSum_nat_sinKernel a ht).tsum_eq]
  apply tsum_of_norm_bounded (g := fun n ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)
  · exact (HurwitzKernelBounds.summable_f_nat 1 0 ht).hasSum.mul_left _
  · intro n
    rw [norm_mul, norm_mul, norm_mul, norm_two, mul_assoc, mul_assoc,
      mul_le_mul_iff_of_pos_left two_pos, HurwitzKernelBounds.f_nat, pow_one, add_zero,
      norm_of_nonneg (exp_pos _).le, Real.norm_eq_abs, Nat.abs_cast, ← mul_assoc,
      mul_le_mul_iff_of_pos_right (exp_pos _)]
    exact mul_le_of_le_one_right (Nat.cast_nonneg _) (abs_sin_le_one _)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
r : ℝ
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ oddKernel a) x - 0) fun (x : ℝ) ↦ x ^ r
have let : ∀ (v : ℝ) (hv : 0 < v) (hv' : IsBigO (F := ℝ) atTop (oddKernel a) fun (x : ℝ) ↦ rexp (-v * x)),
  IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ oddKernel a) x - 0) fun (x : ℝ) ↦ x ^ r
Tactic: let ⟨v, hv, hv'⟩ := isBigO_atTop_oddKernel a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : IsBigO (F := ℝ) atTop (oddKernel a) fun (x : ℝ) ↦ rexp (-v * x)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ oddKernel a) x - 0) fun (x : ℝ) ↦ x ^ r
have rw : ∀ (hv' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖oddKernel a x‖) fun (x : ℝ) ↦ rexp (-v * x)),
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(ofReal ∘ oddKernel a) x - 0‖) fun (x : ℝ) ↦ x ^ r
Tactic: rw [← isBigO_norm_left] at hv' ⊢
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
r : ℝ
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ sinKernel a) x - 0) fun (x : ℝ) ↦ x ^ r
have let : ∀ (v : ℝ) (hv : 0 < v) (hv' : IsBigO (F := ℝ) atTop (sinKernel a) fun (x : ℝ) ↦ rexp (-v * x)),
  IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ sinKernel a) x - 0) fun (x : ℝ) ↦ x ^ r
Tactic: let ⟨v, hv, hv'⟩ := isBigO_atTop_sinKernel a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : IsBigO (F := ℝ) atTop (sinKernel a) fun (x : ℝ) ↦ rexp (-v * x)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ sinKernel a) x - 0) fun (x : ℝ) ↦ x ^ r
have rw : ∀ (hv' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖sinKernel a x‖) fun (x : ℝ) ↦ rexp (-v * x)),
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(ofReal ∘ sinKernel a) x - 0‖) fun (x : ℝ) ↦ x ^ r
Tactic: rw [← isBigO_norm_left] at hv' ⊢
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = (↑(3 / 2) : ℂ) - (s + 1) / 2
have push_cast : (1 - s + 1) / 2 = HDiv.hDiv (α := ℂ) 3 2 - (s + 1) / 2
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = (↑(3 / 2) : ℂ) - (s + 1) / 2
have ring : (1 - s + 1) / 2 = HDiv.hDiv (α := ℂ) 3 2 - (s + 1) / 2
Tactic: { push_cast; ring }
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s
have rw : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = completedSinZeta a s
Tactic: rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = completedSinZeta a s
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s
have rw₁ : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
Tactic: rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = completedSinZeta a s
rw₁ : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s
have rw₂ : (hurwitzOddFEPair a).Λ ((↑(3 / 2) : ℂ) - (s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
Tactic: rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = completedSinZeta a s
rw₁ : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₂ : (hurwitzOddFEPair a).Λ ((↑(3 / 2) : ℂ) - (s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s
have rw₃ : (hurwitzOddFEPair a).Λ ((↑(hurwitzOddFEPair a).k : ℂ) - (s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
Tactic: rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = completedSinZeta a s
rw₁ : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₂ : (hurwitzOddFEPair a).Λ ((↑(3 / 2) : ℂ) - (s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₃ :
  (hurwitzOddFEPair a).Λ ((↑(hurwitzOddFEPair a).k : ℂ) - (s + 1) / 2) / 2 =
    (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₄ : UnitAddCircle
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s
have rw₅ : (hurwitzOddFEPair a).ε • (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
Tactic: rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = completedSinZeta a s
rw₁ : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₂ : (hurwitzOddFEPair a).Λ ((↑(3 / 2) : ℂ) - (s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₃ :
  (hurwitzOddFEPair a).Λ ((↑(hurwitzOddFEPair a).k : ℂ) - (s + 1) / 2) / 2 =
    (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₄ : UnitAddCircle
rw₅ :
  (hurwitzOddFEPair a).ε • (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s
have rw₆ : HSMul.hSMul (α := ℂ) 1 ((hurwitzOddFEPair a).symm.Λ ((s + 1) / 2)) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
Tactic: rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = completedSinZeta a s
rw₁ : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₂ : (hurwitzOddFEPair a).Λ ((↑(3 / 2) : ℂ) - (s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₃ :
  (hurwitzOddFEPair a).Λ ((↑(hurwitzOddFEPair a).k : ℂ) - (s + 1) / 2) / 2 =
    (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₄ : UnitAddCircle
rw₅ :
  (hurwitzOddFEPair a).ε • (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₆ :
  HSMul.hSMul (α := ℂ) 1 ((hurwitzOddFEPair a).symm.Λ ((s + 1) / 2)) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s
have rw₇ : (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
Tactic: rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = (↑(2 * π * a * (↑n : ℝ)) : ℂ) * I
have push_cast : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = (↑(2 * π * a * (↑n : ℝ)) : ℂ) * I
have ring : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I
Tactic: { push_cast; ring }
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
simp_rw : ‖-I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2‖ = 1 / 2
⊢ ‖c n‖ = 1 / 2
have simp_rw₁ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) / 2‖ = 1 / 2
Tactic: simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
simp_rw : ‖-I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2‖ = 1 / 2
simp_rw₁ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) / 2‖ = 1 / 2
⊢ ‖c n‖ = 1 / 2
have simp_rw₂ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / Norm.norm (E := ℂ) 2 = 1 / 2
Tactic: simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
simp_rw : ‖-I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2‖ = 1 / 2
simp_rw₁ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) / 2‖ = 1 / 2
simp_rw₂ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / Norm.norm (E := ℂ) 2 = 1 / 2
⊢ ‖c n‖ = 1 / 2
have simp_rw₃ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
Tactic: simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
simp_rw : ‖-I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2‖ = 1 / 2
simp_rw₁ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) / 2‖ = 1 / 2
simp_rw₂ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / Norm.norm (E := ℂ) 2 = 1 / 2
simp_rw₃ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
⊢ ‖c n‖ = 1 / 2
have simp_rw₄ : ‖-I‖ * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
Tactic: simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
simp_rw : ‖-I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2‖ = 1 / 2
simp_rw₁ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) / 2‖ = 1 / 2
simp_rw₂ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / Norm.norm (E := ℂ) 2 = 1 / 2
simp_rw₃ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₄ : ‖-I‖ * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
⊢ ‖c n‖ = 1 / 2
have simp_rw₅ : ‖I‖ * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
Tactic: simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
simp_rw : ‖-I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2‖ = 1 / 2
simp_rw₁ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) / 2‖ = 1 / 2
simp_rw₂ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / Norm.norm (E := ℂ) 2 = 1 / 2
simp_rw₃ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₄ : ‖-I‖ * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₅ : ‖I‖ * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
⊢ ‖c n‖ = 1 / 2
have simp_rw₆ : 1 * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
Tactic: simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
simp_rw : ‖-I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2‖ = 1 / 2
simp_rw₁ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) / 2‖ = 1 / 2
simp_rw₂ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / Norm.norm (E := ℂ) 2 = 1 / 2
simp_rw₃ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₄ : ‖-I‖ * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₅ : ‖I‖ * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₆ : 1 * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
⊢ ‖c n‖ = 1 / 2
have simp_rw₇ : ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
Tactic: simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]