awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
refine :
  (HDiv.hDiv (α := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) fun (s : ℂ) ↦ s * s.Gammaℝ) =ᶠ[𝓝[≠] 0] fun (s : ℂ) ↦ Λ s / s.Gammaℝ
⊢ Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))

Tactic:
refine Tendsto.congr' ?_ (h_lim.div Gammaℝ_residue_zero two_ne_zero)

Premises used: Filter.Tendsto.div, two_ne_zero, Complex.Gammaℝ_residue_zero, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : ℂ
h :
  ∀ (hs : s ≠ 0),
    HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ
⊢ Membership.mem (γ := Set ℂ) {0}ᶜ s →
    HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ

Tactic:
(hs : s ≠ 0)
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
h :
  ∀ (s : ℂ) (hs : s ≠ 0),
    HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ
⊢ (HDiv.hDiv (α := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) fun (s : ℂ) ↦ s * s.Gammaℝ) =ᶠ[𝓝[≠] 0] fun (s : ℂ) ↦ Λ s / s.Gammaℝ

Tactic:
filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ 0)

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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ℝ
h₂ h₃ : Λ s / s.Gammaℝ = Λ s / s.Gammaℝ
⊢ HDiv.hDiv (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (s : ℂ) ↦ s * Λ s) (fun (s : ℂ) ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ

Tactic:
rw [Pi.div_apply, ← div_div, mul_div_cancel_left₀ _ hs]

Premises used: mul_div_cancel_left₀, Pi.div_apply, div_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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))

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]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
inr :
  ∀ (hs' : Ne (α := ℂ) 0 1),
    DifferentiableAt ℂ (E := ℂ) (F := ℂ)
      (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2)) 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

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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

Tactic:
(claim s hs hs').congr_of_eventuallyEq ?_

Premises used: DifferentiableAt.congr_of_eventuallyEq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
inl :
  (𝓝 s).EventuallyEq (β := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2))
    fun (u : ℂ) ↦ Λ u / u.Gammaℝ
⊢ DifferentiableAt ℂ (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s

Tactic:
refine (claim s hs hs').congr_of_eventuallyEq ?_

Premises used: DifferentiableAt.congr_of_eventuallyEq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
h :
  ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) {0}ᶜ x),
    Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2) x = Λ x / x.Gammaℝ
⊢ (𝓝 s).EventuallyEq (β := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2))
    fun (u : ℂ) ↦ Λ u / u.Gammaℝ

Tactic:
filter_upwards [isOpen_compl_singleton.mem_nhds hs] with x hx

Premises used: isOpen_compl_singleton, IsOpen.mem_nhds
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
x : ℂ
hx : Membership.mem (γ := Set ℂ) {0}ᶜ x
⊢ Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2) x = Λ x / x.Gammaℝ

Tactic:
simp [Function.update_of_ne hx]

Premises used: Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
inr :
  DifferentiableAt ℂ (E := ℂ) (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0
      (limUnder (𝓝[≠] 0) fun (s : ℂ) ↦ Λ s / s.Gammaℝ))
    0
⊢ DifferentiableAt ℂ (E := ℂ) (F := ℂ) (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0 (L / 2))
    0

Tactic:
simp_rw [← claim2.limUnder_eq]

Premises used: Filter.Tendsto.limUnder_eq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
⊢ Membership.mem (γ := Filter ℂ) (𝓝 0) {1}ᶜ

Tactic:
have S_nhds : {(1 : ℂ)}ᶜ ∈ 𝓝 (0 : ℂ) := isOpen_compl_singleton.mem_nhds hs'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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

Tactic:
((Complex.differentiableOn_update_limUnder_of_isLittleO S_nhds
      (fun t ht ↦ (claim t ht.2 ht.1).differentiableWithinAt) ?_) 0 hs').differentiableAt S_nhds

Premises used: DifferentiableWithinAt.differentiableAt, Complex.differentiableOn_update_limUnder_of_isLittleO, DifferentiableAt.differentiableWithinAt, And.right, And.left, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (z : ℂ) ↦ Λ z / z.Gammaℝ - Λ 0 / Gammaℝ 0) fun (z : ℂ) ↦ (z - 0)⁻¹
⊢ DifferentiableAt ℂ (E := ℂ) (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) 0
      (limUnder (𝓝[≠] 0) fun (s : ℂ) ↦ Λ s / s.Gammaℝ))
    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

Premises used: DifferentiableWithinAt.differentiableAt, Complex.differentiableOn_update_limUnder_of_isLittleO, DifferentiableAt.differentiableWithinAt, And.right, And.left, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 :
  IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (z : ℂ) ↦ Λ z / ((↑π : ℂ) ^ (-z / 2) * Complex.Gamma (z / 2))) fun (z : ℂ) ↦
    z⁻¹
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (z : ℂ) ↦ Λ z / z.Gammaℝ - Λ 0 / Gammaℝ 0) fun (z : ℂ) ↦ (z - 0)⁻¹

Tactic:
simp only [Gammaℝ, zero_div, div_zero, Complex.Gamma_zero, mul_zero, sub_zero]

Premises used: sub_zero, Complex.Gammaℝ, zero_div, MulZeroClass.mul_zero, div_zero, Complex.Gamma_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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⁻¹

Tactic:
(isBigO_const_of_tendsto claim2 <| one_ne_zero' ℂ).trans_isLittleO ?_

Premises used: one_ne_zero', Complex.Gammaℝ, Asymptotics.isBigO_const_of_tendsto, Asymptotics.IsBigO.trans_isLittleO, Complex
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (_x : ℂ) ↦ 1) fun (z : ℂ) ↦ z⁻¹
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (z : ℂ) ↦ Λ z / ((↑π : ℂ) ^ (-z / 2) * Complex.Gamma (z / 2))) fun (z : ℂ) ↦
    z⁻¹

Tactic:
refine (isBigO_const_of_tendsto claim2 <| one_ne_zero' ℂ).trans_isLittleO ?_

Premises used: one_ne_zero', Asymptotics.isBigO_const_of_tendsto, Asymptotics.IsBigO.trans_isLittleO, Complex
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
inr₁ : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, x⁻¹ = 0 → Eq (α := ℂ) 1 0
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (_x : ℂ) ↦ 1) fun (z : ℂ) ↦ z⁻¹

Tactic:
rw [isLittleO_iff_tendsto']

Premises used: Asymptotics.isLittleO_iff_tendsto'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
rw₁ rw₂ : x = x
⊢ x = 1 / x⁻¹

Tactic:
rw [← one_div, one_div_one_div]

Premises used: one_div, one_div_one_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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}ᶜ
⊢ Tendsto (β := ℂ) (fun (x : ℂ) ↦ 1 / x⁻¹) (𝓝[≠] 0) (𝓝 0)

Tactic:
exact Tendsto.congr (fun x ↦ by rw [← one_div, one_div_one_div]) nhdsWithin_le_nhds
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : ℂ) in 𝓝[≠] 0, x⁻¹ = 0 → Eq (α := ℂ) 1 0

Tactic:
eventually_of_mem self_mem_nhdsWithin fun x hx hx' ↦ (hx <| inv_eq_zero.mp hx').elim

Premises used: inv_eq_zero, False.elim, Filter.eventually_of_mem, self_mem_nhdsWithin, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : ℂ) in 𝓝[≠] 0, x⁻¹ = 0 → Eq (α := ℂ) 1 0

Tactic:
exact eventually_of_mem self_mem_nhdsWithin fun x hx hx' ↦ (hx <| inv_eq_zero.mp hx').elim
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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ℝ
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
⊢ 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

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
h' : s ≠ 0
inl inl₁ : completedHurwitzZetaEven a s / s.Gammaℝ = 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ℝ

Tactic:
rw [Function.update_of_ne h']

Premises used: Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
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:
simpa [Gammaℝ] using h

Premises used: Complex.Gammaℝ
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ hurwitzZetaEven a 0 = if a = 0 then -1 / 2 else 0

Tactic:
Function.update_self ..

Premises used: Function.update_self, HurwitzZeta.hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven (-a) s = hurwitzZetaEven a s

Tactic:
simp [hurwitzZetaEven]

Premises used: HurwitzZeta.hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
n : ℕ
⊢ -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)
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = -HMul.hMul (α := ℂ) 2 (↑(n + 1) : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : ℂ)
rw₁ : completedHurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1).Gammaℝ = 0
rw₂ : completedHurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / 0 = 0
rw₃ rw₄ : Eq (α := ℂ) 0 0
⊢ hurwitzZetaEven a (-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]

Premises used: Iff.mpr, Complex.Gammaℝ_eq_zero_iff, HAdd.hAdd, Exists.intro, OfNat.ofNat, HurwitzZeta.hurwitzZetaEven, div_zero, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (HDiv.hDiv (α := ℂ) (if a = 0 then -1 else 0) 2))
    s

Tactic:
have := differentiableAt_update_of_residue
    (fun t ht ht' ↦ differentiableAt_completedHurwitzZetaEven a (Or.inl ht) ht')
    (completedHurwitzZetaEven_residue_zero a) s hs'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (HDiv.hDiv (α := ℂ) (if a = 0 then -1 else 0) 2))
    s
⊢ DifferentiableAt ℂ (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (if a = 0 then -1 / 2 else 0))
    s

Tactic:
simp_rw [div_eq_mul_inv, ite_mul, zero_mul, ← div_eq_mul_inv] at this

Premises used: MulZeroClass.zero_mul, div_eq_mul_inv, ite_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (if a = 0 then -1 / 2 else 0))
    s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
this

Premises used: HurwitzZeta.hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (if a = 0 then -1 / 2 else 0))
    s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
exact this
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)

Tactic:
simpa only [Gammaℝ_one, inv_one, mul_one] using (completedHurwitzZetaEven_residue_one a).mul
      <| (differentiable_Gammaℝ_inv.continuous.tendsto _).mono_left nhdsWithin_le_nhds

Premises used: inv_one, HurwitzZeta.completedHurwitzZetaEven_residue_one, Complex.differentiable_Gammaℝ_inv, Continuous.tendsto, Filter.Tendsto.mul, Complex.Gammaℝ_one, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, mul_one, Differentiable.continuous
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)

Tactic:
have : Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s / Gammaℝ s) (𝓝[≠] 1) (𝓝 1) := by
    simpa only [Gammaℝ_one, inv_one, mul_one] using (completedHurwitzZetaEven_residue_one a).mul
      <| (differentiable_Gammaℝ_inv.continuous.tendsto _).mono_left nhdsWithin_le_nhds
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
this : Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
this.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
this : Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
refine :
  EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) fun (s : ℂ) ↦
    (s - 1) * hurwitzZetaEven a s
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
refine this.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
this : Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
h : ∀ (s : ℂ) (hs : s ≠ 0), (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ = (s - 1) * hurwitzZetaEven a s
⊢ EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) fun (s : ℂ) ↦
    (s - 1) * hurwitzZetaEven a s

Tactic:
filter_upwards [eventually_ne_nhdsWithin one_ne_zero] with s hs

Premises used: eventually_ne_nhdsWithin, one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
this : Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
s : ℂ
hs : s ≠ 0
⊢ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ = (s - 1) * hurwitzZetaEven a s

Tactic:
simp [hurwitzZetaEven_def_of_ne_or_ne (Or.inr hs), mul_div_assoc]

Premises used: HurwitzZeta.hurwitzZetaEven_def_of_ne_or_ne, mul_div_assoc, Or.inr