awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  ((hurwitzEvenFEPair a).ε⁻¹ / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₁ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / ((↑(1 / 2) : ℂ) - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₂ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
⊢ ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
have e_a₃ : HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
  (if a = 0 then 1 else 0) / (1 - s)
Tactic: simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
      mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  ((hurwitzEvenFEPair a).ε⁻¹ / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₁ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / ((↑(1 / 2) : ℂ) - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₂ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₃ :
  HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
⊢ ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
have e_a₄ : (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * if a = 0 then 1 else 0) / 2 = (if a = 0 then 1 else 0) / (1 - s)
Tactic: simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
      mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  ((hurwitzEvenFEPair a).ε⁻¹ / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₁ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / ((↑(1 / 2) : ℂ) - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₂ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₃ :
  HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₄ : (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * if a = 0 then 1 else 0) / 2 = (if a = 0 then 1 else 0) / (1 - s)
⊢ ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
have e_a₅ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) / 2 = (if a = 0 then 1 else 0) / (1 - s)
Tactic: simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
      mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  ((hurwitzEvenFEPair a).ε⁻¹ / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₁ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / ((↑(1 / 2) : ℂ) - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₂ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₃ :
  HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₄ : (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * if a = 0 then 1 else 0) / 2 = (if a = 0 then 1 else 0) / (1 - s)
e_a₅ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) / 2 = (if a = 0 then 1 else 0) / (1 - s)
⊢ ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
have e_a₆ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) / 2) = (if a = 0 then 1 else 0) / (1 - s)
Tactic: simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
      mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  ((hurwitzEvenFEPair a).ε⁻¹ / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₁ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / ((↑(1 / 2) : ℂ) - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₂ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₃ :
  HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₄ : (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * if a = 0 then 1 else 0) / 2 = (if a = 0 then 1 else 0) / (1 - s)
e_a₅ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) / 2 = (if a = 0 then 1 else 0) / (1 - s)
e_a₆ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) / 2) = (if a = 0 then 1 else 0) / (1 - s)
⊢ ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
have e_a₇ : (if a = 0 then 1 else 0) * (1 / ((HDiv.hDiv (α := ℂ) 1 2 - s / 2) * 2)) = (if a = 0 then 1 else 0) / (1 - s)
Tactic: simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
      mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  ((hurwitzEvenFEPair a).ε⁻¹ / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₁ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / ((↑(1 / 2) : ℂ) - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₂ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₃ :
  HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₄ : (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * if a = 0 then 1 else 0) / 2 = (if a = 0 then 1 else 0) / (1 - s)
e_a₅ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) / 2 = (if a = 0 then 1 else 0) / (1 - s)
e_a₆ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) / 2) = (if a = 0 then 1 else 0) / (1 - s)
e_a₇ : (if a = 0 then 1 else 0) * (1 / ((HDiv.hDiv (α := ℂ) 1 2 - s / 2) * 2)) = (if a = 0 then 1 else 0) / (1 - s)
⊢ ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
have e_a₈ : (if a = 0 then 1 else 0) * (1 / ((1 - s) / 2 * 2)) = (if a = 0 then 1 else 0) / (1 - s)
Tactic: simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
      mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  ((hurwitzEvenFEPair a).ε⁻¹ / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₁ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / ((↑(1 / 2) : ℂ) - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₂ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₃ :
  HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₄ : (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * if a = 0 then 1 else 0) / 2 = (if a = 0 then 1 else 0) / (1 - s)
e_a₅ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) / 2 = (if a = 0 then 1 else 0) / (1 - s)
e_a₆ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) / 2) = (if a = 0 then 1 else 0) / (1 - s)
e_a₇ : (if a = 0 then 1 else 0) * (1 / ((HDiv.hDiv (α := ℂ) 1 2 - s / 2) * 2)) = (if a = 0 then 1 else 0) / (1 - s)
e_a₈ : (if a = 0 then 1 else 0) * (1 / ((1 - s) / 2 * 2)) = (if a = 0 then 1 else 0) / (1 - s)
⊢ ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
have e_a₉ : (if a = 0 then 1 else 0) * (1 / (1 - s)) = (if a = 0 then 1 else 0) / (1 - s)
Tactic: simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
      mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
have rw : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = completedCosZeta a s
Tactic: rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = completedCosZeta a s
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
have rw₁ : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = completedCosZeta a s
rw₁ : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
have rw₂ : (hurwitzEvenFEPair a).Λ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = completedCosZeta a s
rw₁ : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
have rw₃ : (hurwitzEvenFEPair a).Λ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = completedCosZeta a s
rw₁ : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
have rw₄ : (hurwitzEvenFEPair a).Λ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = completedCosZeta a s
rw₁ : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₄ : (hurwitzEvenFEPair a).Λ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
have rw₅ : (hurwitzEvenFEPair a).ε • (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = completedCosZeta a s
rw₁ : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₄ : (hurwitzEvenFEPair a).Λ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₅ : (hurwitzEvenFEPair a).ε • (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
have rw₆ : HSMul.hSMul (α := ℂ) 1 ((hurwitzEvenFEPair a).symm.Λ (s / 2)) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = completedCosZeta a s
rw₁ : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₄ : (hurwitzEvenFEPair a).Λ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₅ : (hurwitzEvenFEPair a).ε • (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₆ : HSMul.hSMul (α := ℂ) 1 ((hurwitzEvenFEPair a).symm.Λ (s / 2)) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
have rw₇ : (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s
have rw : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
Tactic: rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s
have rw₁ : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
rw₁ : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s
have rw₂ : (hurwitzEvenFEPair a).Λ₀ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
rw₁ : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ₀ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s
have rw₃ : (hurwitzEvenFEPair a).Λ₀ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
rw₁ : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ₀ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ₀ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s
have rw₄ : (hurwitzEvenFEPair a).Λ₀ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
rw₁ : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ₀ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ₀ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₄ : (hurwitzEvenFEPair a).Λ₀ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s
have rw₅ : (hurwitzEvenFEPair a).ε • (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
rw₁ : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ₀ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ₀ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₄ : (hurwitzEvenFEPair a).Λ₀ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₅ : (hurwitzEvenFEPair a).ε • (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s
have rw₆ : HSMul.hSMul (α := ℂ) 1 ((hurwitzEvenFEPair a).symm.Λ₀ (s / 2)) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
rw₁ : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ₀ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ₀ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₄ : (hurwitzEvenFEPair a).Λ₀ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₅ : (hurwitzEvenFEPair a).ε • (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₆ : HSMul.hSMul (α := ℂ) 1 ((hurwitzEvenFEPair a).symm.Λ₀ (s / 2)) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s
have rw₇ : (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
Tactic: rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedCosZeta a (1 - s) = completedHurwitzZetaEven a s
have rw : completedHurwitzZetaEven a (1 - (1 - s)) = completedHurwitzZetaEven a s
Tactic: rw [← completedHurwitzZetaEven_one_sub, sub_sub_cancel]