awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦ rexp (-v * x)
| IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦ rexp (-v * x)
have h : ∀ (x : ℝ), ‖(↑(evenKernel a x) : ℂ) - if a = 0 then 1 else 0‖
Tactic: enter [2, x]; rw [← norm_real, ofReal_sub, apply_ite ((↑) : ℝ → ℂ), ofReal_one, ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦ rexp (-v * x)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(ofReal ∘ evenKernel a) x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦
    x ^ r
have hv'₁ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(↑(evenKernel a x) : ℂ) - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦
  rexp (-v * x)
Tactic: conv at hv' =>
      enter [2, x]; rw [← norm_real, ofReal_sub, apply_ite ((↑) : ℝ → ℂ), ofReal_one, ofReal_zero]
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
r : ℝ
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ cosKernel a) x - 1) fun (x : ℝ) ↦ x ^ r
have obtain : ∀ (p : ℝ) (hp : 0 < p)
  (hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel a x - 1) fun (x : ℝ) ↦ rexp (-p * x)),
  IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ cosKernel a) x - 1) fun (x : ℝ) ↦ x ^ r
Tactic: obtain ⟨p, hp, hp'⟩ := isBigO_atTop_cosKernel_sub a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
⊢ {
      f :=
        WeakFEPair.g
          { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
            f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
            hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
            WeakFEPair ℂ },
      g :=
        WeakFEPair.f
          { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
            f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
            hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
            WeakFEPair ℂ },
      k :=
        WeakFEPair.k
          { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
            f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
            hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
            WeakFEPair ℂ },
      ε :=
        (WeakFEPair.ε
            { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
              f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
              hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
              WeakFEPair ℂ })⁻¹,
      f₀ :=
        WeakFEPair.g₀
          { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
            f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
            hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
            WeakFEPair ℂ },
      g₀ :=
        WeakFEPair.f₀
          { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
            f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
            hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
            WeakFEPair ℂ },
      hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ } =
    { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
      f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
      hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }
have e_f : WeakFEPair.g
    { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
      f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := sorry, hg_int := sorry,
      hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry :
      WeakFEPair ℂ } =
  ofReal ∘ evenKernel 0
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ Eq (α := WeakFEPair ℂ)
    { f := ofReal ∘ evenKernel (-a), g := ofReal ∘ cosKernel (-a), k := 1 / 2, ε := 1, f₀ := if -a = 0 then 1 else 0,
      g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }
    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1, f₀ := if a = 0 then 1 else 0, g₀ := 1,
      hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }
have e_f : ofReal ∘ evenKernel (-a) = ofReal ∘ evenKernel a
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
e_f : ofReal ∘ evenKernel (-a) = ofReal ∘ evenKernel a
⊢ Eq (α := WeakFEPair ℂ)
    { f := ofReal ∘ evenKernel (-a), g := ofReal ∘ cosKernel (-a), k := 1 / 2, ε := 1, f₀ := if -a = 0 then 1 else 0,
      g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }
    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1, f₀ := if a = 0 then 1 else 0, g₀ := 1,
      hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }
have e_g : ofReal ∘ cosKernel (-a) = ofReal ∘ cosKernel a
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
e_f : ofReal ∘ evenKernel (-a) = ofReal ∘ evenKernel a
e_g : ofReal ∘ cosKernel (-a) = ofReal ∘ cosKernel a
⊢ Eq (α := WeakFEPair ℂ)
    { f := ofReal ∘ evenKernel (-a), g := ofReal ∘ cosKernel (-a), k := 1 / 2, ε := 1, f₀ := if -a = 0 then 1 else 0,
      g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }
    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1, f₀ := if a = 0 then 1 else 0, g₀ := 1,
      hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }
have e_f₀ : Eq (α := ℂ) (if -a = 0 then 1 else 0) (if a = 0 then 1 else 0)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven a s = completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)
have rw : (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 -
    ((hurwitzEvenFEPair a).ε / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)
Tactic: rw [completedHurwitzZetaEven, WeakFEPair.Λ, sub_div, sub_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 -
      ((hurwitzEvenFEPair a).ε / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)
have e_a : (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 -
      ((hurwitzEvenFEPair a).ε / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)
have e_a₁ : ((hurwitzEvenFEPair a).ε / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 = 1 / (1 - s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
have e_a : completedHurwitzZetaEven₀ a s - HSMul.hSMul (β := ℂ) (1 / (s / 2)) (if a = 0 then 1 else 0) / 2 =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
Tactic: change completedHurwitzZetaEven₀ a s - (1 / (s / 2)) • (if a = 0 then 1 else 0) / 2 =
      completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a s - HSMul.hSMul (β := ℂ) (1 / (s / 2)) (if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
have e_a : completedHurwitzZetaEven₀ a s - (1 / (s / 2) * if a = 0 then 1 else 0) / 2 =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
Tactic: rw [smul_eq_mul, mul_comm, mul_div_assoc, div_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 :
  completedHurwitzZetaEven₀ a s - (1 / (s / 2) * if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
⊢ completedHurwitzZetaEven₀ a s - HSMul.hSMul (β := ℂ) (1 / (s / 2)) (if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
have e_a₁ : completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2)) / 2 =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
Tactic: rw [smul_eq_mul, mul_comm, mul_div_assoc, div_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 :
  completedHurwitzZetaEven₀ a s - (1 / (s / 2) * if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₁ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2)) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
⊢ completedHurwitzZetaEven₀ a s - HSMul.hSMul (β := ℂ) (1 / (s / 2)) (if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
have e_a₂ : completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2) / 2) =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
Tactic: rw [smul_eq_mul, mul_comm, mul_div_assoc, div_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 :
  completedHurwitzZetaEven₀ a s - (1 / (s / 2) * if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₁ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2)) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₂ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2) / 2) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
⊢ completedHurwitzZetaEven₀ a s - HSMul.hSMul (β := ℂ) (1 / (s / 2)) (if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
have e_a₃ : completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2 * 2)) =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
Tactic: rw [smul_eq_mul, mul_comm, mul_div_assoc, div_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 :
  completedHurwitzZetaEven₀ a s - (1 / (s / 2) * if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₁ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2)) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₂ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2) / 2) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₃ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2 * 2)) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
⊢ completedHurwitzZetaEven₀ a s - HSMul.hSMul (β := ℂ) (1 / (s / 2)) (if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
have e_a₄ : completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / s) =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
Tactic: rw [smul_eq_mul, mul_comm, mul_div_assoc, div_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 :
  completedHurwitzZetaEven₀ a s - (1 / (s / 2) * if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₁ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2)) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₂ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2) / 2) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₃ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2 * 2)) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₄ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / s) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
⊢ completedHurwitzZetaEven₀ a s - HSMul.hSMul (β := ℂ) (1 / (s / 2)) (if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
have e_a₅ : completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
Tactic: rw [smul_eq_mul, mul_comm, mul_div_assoc, div_div, div_mul_cancel₀ _ two_ne_zero, mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ HSMul.hSMul (β := ℂ) (1 / ((↑(1 / 2) : ℂ) - s / 2)) 1 / 2 = 1 / (1 - s)
have e_a : HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) 1 / 2 = 1 / (1 - s)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) 1 / 2 = 1 / (1 - s)
have e_a : 1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * 1 / 2 = 1 / (1 - s)
Tactic: rw [smul_eq_mul, mul_one, ← sub_div, div_div, div_mul_cancel₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a : 1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * 1 / 2 = 1 / (1 - s)
⊢ HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) 1 / 2 = 1 / (1 - s)
have e_a₁ : 1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) / 2 = 1 / (1 - s)
Tactic: rw [smul_eq_mul, mul_one, ← sub_div, div_div, div_mul_cancel₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a : 1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * 1 / 2 = 1 / (1 - s)
e_a₁ : 1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) / 2 = 1 / (1 - s)
⊢ HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) 1 / 2 = 1 / (1 - s)
have e_a₂ : 1 / ((1 - s) / 2) / 2 = 1 / (1 - s)
Tactic: rw [smul_eq_mul, mul_one, ← sub_div, div_div, div_mul_cancel₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a : 1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * 1 / 2 = 1 / (1 - s)
e_a₁ : 1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) / 2 = 1 / (1 - s)
e_a₂ : 1 / ((1 - s) / 2) / 2 = 1 / (1 - s)
⊢ HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) 1 / 2 = 1 / (1 - s)
have e_a₃ : 1 / ((1 - s) / 2 * 2) = 1 / (1 - s)
Tactic: rw [smul_eq_mul, mul_one, ← sub_div, div_div, div_mul_cancel₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a : 1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * 1 / 2 = 1 / (1 - s)
e_a₁ : 1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) / 2 = 1 / (1 - s)
e_a₂ : 1 / ((1 - s) / 2) / 2 = 1 / (1 - s)
e_a₃ : 1 / ((1 - s) / 2 * 2) = 1 / (1 - s)
⊢ HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) 1 / 2 = 1 / (1 - s)
have e_a₄ : 1 / (1 - s) = 1 / (1 - s)
Tactic: rw [smul_eq_mul, mul_one, ← sub_div, div_div, div_mul_cancel₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedCosZeta a s = completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s)
have rw : (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 -
    ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
  completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s)
Tactic: rw [completedCosZeta, WeakFEPair.Λ, sub_div, sub_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 -
      ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ /
        2 =
    completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s)
have e_a : (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
  completedCosZeta₀ a s - 1 / s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    completedCosZeta₀ a s - 1 / s
⊢ (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 -
      ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ /
        2 =
    completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s)
have e_a₁ : ((hurwitzEvenFEPair a).symm.ε / ((↑(hurwitzEvenFEPair a).symm.k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
  (if a = 0 then 1 else 0) / (1 - s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    completedCosZeta₀ a s - 1 / s
have e_a : (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
  (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - 1 / s
Tactic: rw [completedCosZeta₀, WeakFEPair.symm, hurwitzEvenFEPair, smul_eq_mul, mul_one, div_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - 1 / s
⊢ (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    completedCosZeta₀ a s - 1 / s
have e_a₁ : { f := (hurwitzEvenFEPair a).g, g := (hurwitzEvenFEPair a).f, k := (hurwitzEvenFEPair a).k,
            ε := (hurwitzEvenFEPair a).ε⁻¹, f₀ := (hurwitzEvenFEPair a).g₀, g₀ := (hurwitzEvenFEPair a).f₀, hf_int := sorry,
            hg_int := sorry, hk := sorry, hε := sorry, h_feq := sorry, hf_top := sorry, hg_top := sorry : WeakFEPair ℂ }.Λ₀
        (s / 2) /
      2 -
    (1 / (s / 2)) •
        { f := (hurwitzEvenFEPair a).g, g := (hurwitzEvenFEPair a).f, k := (hurwitzEvenFEPair a).k,
            ε := (hurwitzEvenFEPair a).ε⁻¹, f₀ := (hurwitzEvenFEPair a).g₀, g₀ := (hurwitzEvenFEPair a).f₀, hf_int := sorry,
            hg_int := sorry, hk := sorry, hε := sorry, h_feq := sorry, hf_top := sorry, hg_top := sorry : WeakFEPair ℂ }.f₀ /
      2 =
  { f := (hurwitzEvenFEPair a).g, g := (hurwitzEvenFEPair a).f, k := (hurwitzEvenFEPair a).k,
            ε := (hurwitzEvenFEPair a).ε⁻¹, f₀ := (hurwitzEvenFEPair a).g₀, g₀ := (hurwitzEvenFEPair a).f₀, hf_int := sorry,
            hg_int := sorry, hk := sorry, hε := sorry, h_feq := sorry, hf_top := sorry, hg_top := sorry : WeakFEPair ℂ }.Λ₀
        (s / 2) /
      2 -
    1 / s
Tactic: rw [completedCosZeta₀, WeakFEPair.symm, hurwitzEvenFEPair, smul_eq_mul, mul_one, div_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
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 : ((hurwitzEvenFEPair a).ε⁻¹ / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).f₀ / 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)
⊢ ((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⁻¹ / ((↑(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)
⊢ ((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]