awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
⊢ HasSum (α := ℂ) (fun (n : ℤ) ↦ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (mellin
      (fun (t : ℝ) ↦
        ((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
            (↑(if
                    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                      (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                  1
                else 0) :
              ℂ)) /
          2)
      (s / 2))
have refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ / |(↑i : ℝ) + a| ^ s.re
Tactic: refine (hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ / |(↑i : ℝ) + a| ^ s.re
⊢ HasSum (α := ℂ) (fun (n : ℤ) ↦ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (mellin
      (fun (t : ℝ) ↦
        ((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
            (↑(if
                    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                      (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                  1
                else 0) :
              ℂ)) /
          2)
      (s / 2))
have refine_2 : ∀ (n : ℤ), s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 = s.Gammaℝ * (1 / 2) / (↑|(↑n : ℝ) + a| : ℂ) ^ s
Tactic: refine (hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ / |(↑i : ℝ) + a| ^ s.re
have refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ * (1 / |(↑i : ℝ) + a| ^ s.re)
Tactic: simp_rw [← mul_one_div ‖_‖]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ * (1 / |(↑i : ℝ) + a| ^ s.re)
have refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ 1 / |(↑i : ℝ) + a| ^ s.re
Tactic: apply Summable.mul_left
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
n : ℤ
⊢ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 = s.Gammaℝ * (1 / 2) / (↑|(↑n : ℝ) + a| : ℂ) ^ s
have refine_2 : s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 = s.Gammaℝ / 2 / (↑|(↑n : ℝ) + a| : ℂ) ^ s
Tactic: rw [mul_one_div, div_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ))
      (((↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) -
          (↑(if
                  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
                    (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
                1
              else 0) :
            ℂ)) /
        2)
n : ℤ
refine_2 : s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 = s.Gammaℝ / 2 / (↑|(↑n : ℝ) + a| : ℂ) ^ s
⊢ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 = s.Gammaℝ * (1 / 2) / (↑|(↑n : ℝ) + a| : ℂ) ^ s
have refine_2₁ : s.Gammaℝ / 2 / (↑|(↑n : ℝ) + a| : ℂ) ^ s = s.Gammaℝ / 2 / (↑|(↑n : ℝ) + a| : ℂ) ^ s
Tactic: rw [mul_one_div, div_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s
have claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
Tactic: have claim (t) (ht : t ≠ 0) (ht' : t ≠ 1) : DifferentiableAt ℂ (fun u : ℂ ↦ Λ u / Gammaℝ u) t :=
    (hf t ht ht').mul differentiable_Gammaℝ_inv.differentiableAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
⊢ Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
have refine : (HDiv.hDiv (α := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) fun (s : ℂ) ↦ s * s.Gammaℝ) =ᶠ[𝓝[≠] 0] fun (s : ℂ) ↦ Λ s / s.Gammaℝ
Tactic: refine Tendsto.congr' ?_ (h_lim.div Gammaℝ_residue_zero two_ne_zero)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s_1 : ℂ
hs' : s_1 ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
s : ℂ
⊢ Membership.mem (γ := Set ℂ) {0}ᶜ s →
    HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ
have h : ∀ (hs : s ≠ 0),
  HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ
Tactic: (hs : s ≠ 0)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
⊢ (HDiv.hDiv (α := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) fun (s : ℂ) ↦ s * s.Gammaℝ) =ᶠ[𝓝[≠] 0] fun (s : ℂ) ↦ Λ s / s.Gammaℝ
have h : ∀ (s : ℂ) (hs : s ≠ 0),
  HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ
Tactic: filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ 0)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s_1 : ℂ
hs' : s_1 ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
⊢ HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ
have h : s * Λ s / (s * s.Gammaℝ) = Λ s / s.Gammaℝ
Tactic: rw [Pi.div_apply, ← div_div, mul_div_cancel_left₀ _ hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s_1 : ℂ
hs' : s_1 ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
h : s * Λ s / (s * s.Gammaℝ) = Λ s / s.Gammaℝ
⊢ HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ
have h₁ : s * Λ s / s / s.Gammaℝ = Λ s / s.Gammaℝ
Tactic: rw [Pi.div_apply, ← div_div, mul_div_cancel_left₀ _ hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s_1 : ℂ
hs' : s_1 ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
h : s * Λ s / (s * s.Gammaℝ) = Λ s / s.Gammaℝ
h₁ : s * Λ s / s / s.Gammaℝ = Λ s / s.Gammaℝ
⊢ HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ
have h₂ : Λ s / s.Gammaℝ = Λ s / s.Gammaℝ
Tactic: rw [Pi.div_apply, ← div_div, mul_div_cancel_left₀ _ hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
⊢ DifferentiableAt ℂ (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s
have claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
Tactic: have claim2 : Tendsto (fun s : ℂ ↦ Λ s / Gammaℝ s) (𝓝[≠] 0) (𝓝 <| L / 2) := by
    refine Tendsto.congr' ?_ (h_lim.div Gammaℝ_residue_zero two_ne_zero)
    filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ 0)
    rw [Pi.div_apply, ← div_div, mul_div_cancel_left₀ _ hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
⊢ DifferentiableAt ℂ (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s
have inl : ∀ (hs : s ≠ 0),
  DifferentiableAt ℂ (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s
Tactic: rcases ne_or_eq s 0 with hs | rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
inl :
  ∀ (hs : s ≠ 0),
    DifferentiableAt ℂ (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s
⊢ DifferentiableAt ℂ (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s
have inr : ∀ (hs' : Ne (α := ℂ) 0 1),
  DifferentiableAt ℂ (E := ℂ) (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2))
    0
Tactic: rcases ne_or_eq s 0 with hs | rfl
Cleared hypotheses: s, hs'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs : s ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s
have inl : (𝓝 s).EventuallyEq (β := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2))
  fun (u : ℂ) ↦ Λ u / u.Gammaℝ
Tactic: refine (claim s hs hs').congr_of_eventuallyEq ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs : s ≠ 0
⊢ (𝓝 s).EventuallyEq (β := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2))
    fun (u : ℂ) ↦ Λ u / u.Gammaℝ
have h : ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) {0}ᶜ x),
  Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2) x = Λ x / x.Gammaℝ
Tactic: filter_upwards [isOpen_compl_singleton.mem_nhds hs] with x hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : Ne (α := ℂ) 0 1
⊢ DifferentiableAt ℂ (E := ℂ) (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2))
    0
have inr : DifferentiableAt ℂ (E := ℂ) (F := ℂ)
  (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0
    (limUnder (𝓝[≠] 0) fun (s : ℂ) ↦ Λ s / s.Gammaℝ))
  0
Tactic: simp_rw [← claim2.limUnder_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : Ne (α := ℂ) 0 1
⊢ DifferentiableAt ℂ (E := ℂ) (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0
      (limUnder (𝓝[≠] 0) fun (s : ℂ) ↦ Λ s / s.Gammaℝ))
    0
have S_nhds : Membership.mem (γ := Filter ℂ) (𝓝 0) {1}ᶜ
Tactic: have S_nhds : {(1 : ℂ)}ᶜ ∈ 𝓝 (0 : ℂ) := isOpen_compl_singleton.mem_nhds hs'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : Ne (α := ℂ) 0 1
S_nhds : Membership.mem (γ := Filter ℂ) (𝓝 0) {1}ᶜ
⊢ DifferentiableAt ℂ (E := ℂ) (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0
      (limUnder (𝓝[≠] 0) fun (s : ℂ) ↦ Λ s / s.Gammaℝ))
    0
have inr : IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (z : ℂ) ↦ Λ z / z.Gammaℝ - Λ 0 / Gammaℝ 0) fun (z : ℂ) ↦ (z - 0)⁻¹
Tactic: refine ((Complex.differentiableOn_update_limUnder_of_isLittleO S_nhds
      (fun t ht ↦ (claim t ht.2 ht.1).differentiableWithinAt) ?_) 0 hs').differentiableAt S_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : Ne (α := ℂ) 0 1
S_nhds : Membership.mem (γ := Filter ℂ) (𝓝 0) {1}ᶜ
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (z : ℂ) ↦ Λ z / z.Gammaℝ - Λ 0 / Gammaℝ 0) fun (z : ℂ) ↦ (z - 0)⁻¹
have inr : IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (z : ℂ) ↦ Λ z / ((↑π : ℂ) ^ (-z / 2) * Complex.Gamma (z / 2))) fun (z : ℂ) ↦
  z⁻¹
Tactic: simp only [Gammaℝ, zero_div, div_zero, Complex.Gamma_zero, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : Ne (α := ℂ) 0 1
S_nhds : Membership.mem (γ := Filter ℂ) (𝓝 0) {1}ᶜ
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (z : ℂ) ↦ Λ z / ((↑π : ℂ) ^ (-z / 2) * Complex.Gamma (z / 2))) fun (z : ℂ) ↦
    z⁻¹
have inr : IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (_x : ℂ) ↦ 1) fun (z : ℂ) ↦ z⁻¹
Tactic: refine (isBigO_const_of_tendsto claim2 <| one_ne_zero' ℂ).trans_isLittleO ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : Ne (α := ℂ) 0 1
S_nhds : Membership.mem (γ := Filter ℂ) (𝓝 0) {1}ᶜ
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (_x : ℂ) ↦ 1) fun (z : ℂ) ↦ z⁻¹
have inr : Tendsto (β := ℂ) (fun (x : ℂ) ↦ 1 / x⁻¹) (𝓝[≠] 0) (𝓝 0)
Tactic: rw [isLittleO_iff_tendsto']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : Ne (α := ℂ) 0 1
S_nhds : Membership.mem (γ := Filter ℂ) (𝓝 0) {1}ᶜ
inr : Tendsto (β := ℂ) (fun (x : ℂ) ↦ 1 / x⁻¹) (𝓝[≠] 0) (𝓝 0)
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (_x : ℂ) ↦ 1) fun (z : ℂ) ↦ z⁻¹
have inr₁ : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, x⁻¹ = 0 → Eq (α := ℂ) 1 0
Tactic: rw [isLittleO_iff_tendsto']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : Ne (α := ℂ) 0 1
S_nhds : Membership.mem (γ := Filter ℂ) (𝓝 0) {1}ᶜ
x : ℂ
⊢ x = 1 / x⁻¹
have rw : x = 1 / (1 / x)
Tactic: rw [← one_div, one_div_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : Ne (α := ℂ) 0 1
S_nhds : Membership.mem (γ := Filter ℂ) (𝓝 0) {1}ᶜ
x : ℂ
rw : x = 1 / (1 / x)
⊢ x = 1 / x⁻¹
have rw₁ : x = x
Tactic: rw [← one_div, one_div_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
⊢ Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ
have inl : ∀ (h' : s ≠ 0),
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ
Tactic: rcases ne_or_eq s 0 with h' | rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
inl :
  ∀ (h' : s ≠ 0),
    Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
        (if a = 0 then -1 / 2 else 0) s =
      completedHurwitzZetaEven a s / s.Gammaℝ
⊢ Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ
have inr : ∀ (h : a ≠ 0 ∨ Ne (α := ℂ) 0 0),
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (if a = 0 then -1 / 2 else 0) 0 =
    completedHurwitzZetaEven a 0 / Gammaℝ 0
Tactic: rcases ne_or_eq s 0 with h' | rfl
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
h' : s ≠ 0
⊢ Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ
have inl : completedHurwitzZetaEven a s / s.Gammaℝ = completedHurwitzZetaEven a s / s.Gammaℝ
Tactic: rw [Function.update_of_ne h']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
n : ℕ
⊢ hurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
Tactic: have : (-2 : ℂ) * (n + 1) ≠ 0 :=
    mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (Nat.cast_add_one_ne_zero n)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ hurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have rw : Eq (α := ℂ)
  (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (if a = 0 then -1 / 2 else 0) (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) :
    ℂ)
  (0 : ℂ)
Tactic: rw [hurwitzZetaEven, Function.update_of_ne this, Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by simp⟩,
    div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
        (if a = 0 then -1 / 2 else 0) (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) :
      ℂ)
    (0 : ℂ)
⊢ hurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have rw₁ : completedHurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1).Gammaℝ = 0
Tactic: rw [hurwitzZetaEven, Function.update_of_ne this, Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by simp⟩,
    div_zero]