awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
x : ℂ
hs : Membership.mem (γ := Set ℂ) (Set.univ \ {1}) x
⊢ x ≠ 1 ∨ Ne (α := DirichletCharacter ℂ n) 1 1

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
x : ℂ
hs : Membership.mem (γ := Set ℂ) (Set.univ \ {1}) x
funProp : x ≠ 1 ∨ Ne (α := DirichletCharacter ℂ n) 1 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar n s) x

Tactic:
fun_prop (disch := simp_all)
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
refine : ContinuousWithinAt (LFunctionTrivChar₁ n) {1}ᶜ 1
⊢ DifferentiableOn ℂ (LFunctionTrivChar₁ n) (Set.univ \ {1}) ∧ ContinuousAt (LFunctionTrivChar₁ n) 1

Tactic:
refine ⟨DifferentiableOn.congr (f := fun s ↦ (s - 1) * LFunctionTrivChar n s)
    (fun _ hs ↦ DifferentiableAt.differentiableWithinAt <| by fun_prop (disch := simp_all))
    fun _ hs ↦ Function.update_of_ne (Set.mem_diff_singleton.mp hs).2 ..,
    continuousWithinAt_compl_self.mp ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
⊢ ContinuousWithinAt (LFunctionTrivChar₁ n) {1}ᶜ 1

Tactic:
simpa using LFunctionTrivChar_residue_one

Premises used: DirichletCharacter.LFunctionTrivChar_residue_one
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
s : ℂ
hs : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ n) s = deriv (fun (w : ℂ) ↦ (w - 1) * LFunctionTrivChar n w) s

Tactic:
eventuallyEq_iff_exists_mem.mpr ?_ |>.deriv_eq

Premises used: Iff.mpr, Filter.EventuallyEq.deriv_eq, Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
s : ℂ
hs : s ≠ 1
refine : ∃ s_1 ∈ 𝓝 s, Set.EqOn (LFunctionTrivChar₁ n) (fun (w : ℂ) ↦ (w - 1) * LFunctionTrivChar n w) s_1
⊢ deriv (LFunctionTrivChar₁ n) s = deriv (fun (w : ℂ) ↦ (w - 1) * LFunctionTrivChar n w) s

Tactic:
refine eventuallyEq_iff_exists_mem.mpr ?_ |>.deriv_eq

Premises used: Iff.mpr, Filter.EventuallyEq.deriv_eq, Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
s : ℂ
hs : s ≠ 1
⊢ ∃ s_1 ∈ 𝓝 s, Set.EqOn (LFunctionTrivChar₁ n) (fun (w : ℂ) ↦ (w - 1) * LFunctionTrivChar n w) s_1

Tactic:
⟨_, isOpen_ne.mem_nhds hs, fun _ hw ↦ Function.update_of_ne (Set.mem_setOf.mp hw) ..⟩

Premises used: HMul.hMul, HSub.hSub, Nat.cast, Set.mem_setOf, Finset.prod, Inv.inv, isOpen_ne, And.intro, IsOpen.mem_nhds, Exists.intro, Iff.mp, DirichletCharacter.LFunctionTrivChar, Nat.primeFactors, OfNat.ofNat, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
s : ℂ
hs : s ≠ 1
⊢ ∃ s_1 ∈ 𝓝 s, Set.EqOn (LFunctionTrivChar₁ n) (fun (w : ℂ) ↦ (w - 1) * LFunctionTrivChar n w) s_1

Tactic:
exact ⟨_, isOpen_ne.mem_nhds hs, fun _ hw ↦ Function.update_of_ne (Set.mem_setOf.mp hw) ..⟩
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
s : ℂ
hs : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ n) s = deriv (fun (w : ℂ) ↦ (w - 1) * LFunctionTrivChar n w) s

Tactic:
have H : deriv (LFunctionTrivChar₁ n) s =
      deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s := by
    refine eventuallyEq_iff_exists_mem.mpr ?_ |>.deriv_eq
    exact ⟨_, isOpen_ne.mem_nhds hs, fun _ hw ↦ Function.update_of_ne (Set.mem_setOf.mp hw) ..⟩
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun (w : ℂ) ↦ (w - 1) * LFunctionTrivChar n w) s
⊢ DifferentiableAt ℂ (F := ℂ) (fun (w : ℂ) ↦ w - 1) s

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun (w : ℂ) ↦ (w - 1) * LFunctionTrivChar n w) s
rw :
  deriv (fun (w : ℂ) ↦ (w - 1) * LFunctionTrivChar n w) s =
    (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s
rw₁ :
  deriv (fun (w : ℂ) ↦ w - 1) s * LFunction (N := n) 1 s + (s - 1) * deriv (LFunction (N := n) 1) s =
    (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s
rw₂ :
  deriv (fun (w : ℂ) ↦ w) s * LFunction (N := n) 1 s + (s - 1) * deriv (LFunction (N := n) 1) s =
    (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s
rw₃ :
  (fun (x : ℂ) ↦ (1 : ℂ)) s * LFunction (N := n) 1 s + (s - 1) * deriv (LFunction (N := n) 1) s =
    (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s
rw₄ :
  LFunction (N := n) 1 s + (s - 1) * deriv (LFunction (N := n) 1) s =
    (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s
rw₅ rw₆ :
  (s - 1) * deriv (LFunction (N := n) 1) s + LFunction (N := n) 1 s =
    (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s
⊢ deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Tactic:
rw [H, deriv_fun_mul (by fun_prop) (differentiableAt_LFunction _ s (.inl hs)), deriv_sub_const,
    deriv_id'', one_mul, add_comm]

Premises used: deriv_fun_mul, DirichletCharacter.differentiableAt_LFunction, deriv_id'', add_comm, deriv_sub_const, Or.inl, one_mul
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
simp_rw :
  ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
⊢ ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s)
    {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
simp_rw [neg_div]

Premises used: neg_div
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
⊢ Differentiable ℂ (LFunctionTrivChar₁ n)

Tactic:
have h := differentiable_LFunctionTrivChar₁ n
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
⊢ ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
((h.contDiff.continuous_deriv le_rfl).continuousOn.div
    h.continuous.continuousOn fun w hw ↦ ?_).neg

Premises used: ContinuousOn.neg, Continuous.continuousOn, le_rfl, ContDiff.continuous_deriv, ContinuousOn.div, Differentiable.contDiff, Differentiable.continuous
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
refine :
  ∀ (w : ℂ) (hw : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0} w), LFunctionTrivChar₁ n w ≠ 0
⊢ ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
refine ((h.contDiff.continuous_deriv le_rfl).continuousOn.div
    h.continuous.continuousOn fun w hw ↦ ?_).neg

Premises used: ContinuousOn.neg, Continuous.continuousOn, le_rfl, ContDiff.continuous_deriv, ContinuousOn.div, Differentiable.contDiff, Differentiable.continuous
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0} w
inl : ∀ (hw : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0} 1), LFunctionTrivChar₁ n 1 ≠ 0
inr : ∀ (hw' : w ≠ 1), LFunctionTrivChar₁ n w ≠ 0
⊢ LFunctionTrivChar₁ n w ≠ 0

Tactic:
rcases eq_or_ne w 1 with rfl | hw'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
hw : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0} 1
⊢ LFunctionTrivChar₁ n 1 ≠ 0

Tactic:
LFunctionTrivChar₁_apply_one_ne_zero _

Premises used: DirichletCharacter.LFunctionTrivChar₁_apply_one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
hw : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0} 1
⊢ LFunctionTrivChar₁ n 1 ≠ 0

Tactic:
exact LFunctionTrivChar₁_apply_one_ne_zero _

Premises used: DirichletCharacter.LFunctionTrivChar₁_apply_one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0} w
hw' : w ≠ 1
inr : w - 1 ≠ 0 ∧ LFunctionTrivChar n w ≠ 0
⊢ LFunctionTrivChar₁ n w ≠ 0

Tactic:
rw [LFunctionTrivChar₁, Function.update_of_ne hw', mul_ne_zero_iff]

Premises used: DirichletCharacter.LFunctionTrivChar₁, mul_ne_zero_iff, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0} w
hw' : w ≠ 1
⊢ w - 1 ≠ 0 ∧ LFunctionTrivChar n w ≠ 0

Tactic:
⟨sub_ne_zero_of_ne hw', (Set.mem_setOf.mp hw).resolve_left hw'⟩

Premises used: Or.resolve_left, Set.mem_setOf, sub_ne_zero_of_ne, And.intro, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0} w
hw' : w ≠ 1
⊢ w - 1 ≠ 0 ∧ LFunctionTrivChar n w ≠ 0

Tactic:
exact ⟨sub_ne_zero_of_ne hw', (Set.mem_setOf.mp hw).resolve_left hw'⟩
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
χ : DirichletCharacter ℂ n
hχ : χ ≠ 1
⊢ Differentiable ℂ (LFunction χ)

Tactic:
have h := differentiable_LFunction hχ
-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
Goal:
n : ℕ
inst : NeZero n
χ : DirichletCharacter ℂ n
hχ : χ ≠ 1
h : Differentiable ℂ (LFunction χ)
⊢ ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -deriv (LFunction χ) s / LFunction χ s) {s : ℂ | LFunction χ s ≠ 0}

Tactic:
simpa [neg_div] using ((h.contDiff.continuous_deriv le_rfl).continuousOn.div
    h.continuous.continuousOn fun _ hw ↦ hw).neg

Premises used: ContinuousOn.neg, neg_div, Continuous.continuousOn, le_rfl, ContDiff.continuous_deriv, ContinuousOn.div, Differentiable.contDiff, Differentiable.continuous
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
simp :
  hurwitzZetaEven a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s + (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2
⊢ hurwitzZetaEven a s = (hurwitzZeta a s + hurwitzZeta (-a) s) / 2

Tactic:
simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg]

Premises used: HurwitzZeta.hurwitzZeta, HurwitzZeta.hurwitzZetaOdd_neg, HurwitzZeta.hurwitzZetaEven_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s + (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
simp : hurwitzZetaOdd a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s - (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2
⊢ hurwitzZetaOdd a s = (hurwitzZeta a s - hurwitzZeta (-a) s) / 2

Tactic:
simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg]

Premises used: HurwitzZeta.hurwitzZeta, HurwitzZeta.hurwitzZetaOdd_neg, HurwitzZeta.hurwitzZetaEven_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaOdd a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s - (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ (hurwitzZeta a) s

Tactic:
(differentiableAt_hurwitzZetaEven a hs).add (differentiable_hurwitzZetaOdd a s)

Premises used: HurwitzZeta.differentiableAt_hurwitzZetaEven, HurwitzZeta.differentiable_hurwitzZetaOdd, HurwitzZeta.hurwitzZeta, DifferentiableAt.add
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
⊢ HasSum
    (fun (b : ℕ) ↦
      (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 +
        (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2)
    (hurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s + hurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
(hasSum_nat_hurwitzZetaEven_of_mem_Icc ha hs).add (hasSum_nat_hurwitzZetaOdd_of_mem_Icc ha hs)

Premises used: HasSum.add, HurwitzZeta.hasSum_nat_hurwitzZetaEven_of_mem_Icc, HurwitzZeta.hasSum_nat_hurwitzZetaOdd_of_mem_Icc
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s) fun (b : ℕ) ↦
    (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 +
      (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2
⊢ HasSum (fun (n : ℕ) ↦ 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s) (hurwitzZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
convert!
    (hasSum_nat_hurwitzZetaEven_of_mem_Icc ha hs).add (hasSum_nat_hurwitzZetaOdd_of_mem_Icc ha hs)
    using 1

Premises used: HasSum.add, HurwitzZeta.hasSum_nat_hurwitzZetaEven_of_mem_Icc, HurwitzZeta.hasSum_nat_hurwitzZetaOdd_of_mem_Icc
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
h :
  ∀ (n : ℕ),
    1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s =
      (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 +
        (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s) fun (b : ℕ) ↦
    (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 +
      (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
x y : ℂ
⊢ x = (x + y) / 2 + (x - y) / 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s =
    (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 +
      (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2

Tactic:
apply show ∀ (x y : ℂ), x = (x + y) / 2 + (x - y) / 2 by intros; ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
⊢ 𝓝 1 = 𝓝 (1 + HSub.hSub (α := ℂ) 1 1 * hurwitzZetaOdd a 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
simp :
  Tendsto (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1)
    (𝓝 (1 + HSub.hSub (α := ℂ) 1 1 * hurwitzZetaOdd a 1))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
simp only [hurwitzZeta, mul_add, (by simp : 𝓝 (1 : ℂ) = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))]

Premises used: mul_add, HurwitzZeta.hurwitzZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
⊢ Tendsto (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1)
    (𝓝 (1 + HSub.hSub (α := ℂ) 1 1 * hurwitzZetaOdd a 1))

Tactic:
(hurwitzZetaEven_residue_one a).add ((Tendsto.mul ?_ ?_).mono_left nhdsWithin_le_nhds)

Premises used: Filter.Tendsto.mul, nhdsWithin_le_nhds, Filter.Tendsto.add, Filter.Tendsto.mono_left, HurwitzZeta.hurwitzZetaEven_residue_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
refine_1 : Tendsto (fun (s : ℂ) ↦ s - 1) (𝓝 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
refine_2 : Tendsto (hurwitzZetaOdd a) (𝓝 1) (𝓝 (hurwitzZetaOdd a 1))
⊢ Tendsto (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1)
    (𝓝 (1 + HSub.hSub (α := ℂ) 1 1 * hurwitzZetaOdd a 1))

Tactic:
refine (hurwitzZetaEven_residue_one a).add ((Tendsto.mul ?_ ?_).mono_left nhdsWithin_le_nhds)

Premises used: Filter.Tendsto.mul, nhdsWithin_le_nhds, Filter.Tendsto.add, Filter.Tendsto.mono_left, HurwitzZeta.hurwitzZetaEven_residue_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
⊢ Tendsto (fun (s : ℂ) ↦ s - 1) (𝓝 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))

Tactic:
tendsto_id.sub_const _

Premises used: Filter.tendsto_id, Filter.Tendsto.sub_const
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
⊢ Tendsto (hurwitzZetaOdd a) (𝓝 1) (𝓝 (hurwitzZetaOdd a 1))

Tactic:
(differentiable_hurwitzZetaOdd a).continuous.tendsto _

Premises used: HurwitzZeta.differentiable_hurwitzZetaOdd, Continuous.tendsto, Differentiable.continuous
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
⊢ Tendsto (fun (s : ℂ) ↦ s - 1) (𝓝 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))

Tactic:
exacts [tendsto_id.sub_const _, (differentiable_hurwitzZetaOdd a).continuous.tendsto _]

Premises used: Filter.tendsto_id, HurwitzZeta.differentiable_hurwitzZetaOdd, Filter.Tendsto.sub_const, Continuous.tendsto, Differentiable.continuous
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
simp : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
simp only [hurwitzZeta, add_sub_right_comm]

Premises used: add_sub_right_comm, HurwitzZeta.hurwitzZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) 1

Tactic:
(differentiableAt_hurwitzZetaEven_sub_one_div a).add (differentiable_hurwitzZetaOdd a 1)

Premises used: HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, HurwitzZeta.differentiable_hurwitzZetaOdd, OfNat.ofNat, DifferentiableAt.add
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) 1

Tactic:
exact (differentiableAt_hurwitzZetaEven_sub_one_div a).add (differentiable_hurwitzZetaOdd a 1)

Premises used: HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, HurwitzZeta.differentiable_hurwitzZetaOdd, OfNat.ofNat, DifferentiableAt.add
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
simp :
  Tendsto (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) (𝓝 1)
    (𝓝 (hurwitzZetaEven a 1 + hurwitzZetaOdd a 1))
⊢ Tendsto (fun (s : ℂ) ↦ hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZeta a 1))

Tactic:
simp only [hurwitzZeta, add_sub_right_comm]

Premises used: add_sub_right_comm, HurwitzZeta.hurwitzZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
⊢ Tendsto (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) (𝓝 1)
    (𝓝 (hurwitzZetaEven a 1 + hurwitzZetaOdd a 1))

Tactic:
(tendsto_hurwitzZetaEven_sub_one_div_nhds_one a).add
    (differentiable_hurwitzZetaOdd a 1).continuousAt.tendsto

Premises used: HurwitzZeta.differentiable_hurwitzZetaOdd, DifferentiableAt.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.add, OfNat.ofNat, HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
⊢ Tendsto (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) (𝓝 1)
    (𝓝 (hurwitzZetaEven a 1 + hurwitzZetaOdd a 1))

Tactic:
refine (tendsto_hurwitzZetaEven_sub_one_div_nhds_one a).add
    (differentiable_hurwitzZetaOdd a 1).continuousAt.tendsto

Premises used: HurwitzZeta.differentiable_hurwitzZetaOdd, DifferentiableAt.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.add, OfNat.ofNat, HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a b : UnitAddCircle
simp :
  Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦
    hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ hurwitzZeta a s - hurwitzZeta b s

Tactic:
simp only [hurwitzZeta, add_sub_add_comm]

Premises used: add_sub_add_comm, HurwitzZeta.hurwitzZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a b : UnitAddCircle
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦
    hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)

Tactic:
(differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (.sub ?_ ?_)

Premises used: Differentiable.sub, Differentiable.add, HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a b : UnitAddCircle
refine_1 : Differentiable ℂ (hurwitzZetaOdd a)
refine_2 : Differentiable ℂ (hurwitzZetaOdd b)
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦
    hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)

Tactic:
refine (differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (.sub ?_ ?_)

Premises used: Differentiable.sub, Differentiable.add, HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd a)

Tactic:
apply differentiable_hurwitzZetaOdd

Premises used: HurwitzZeta.differentiable_hurwitzZetaOdd
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd b)

Tactic:
apply differentiable_hurwitzZetaOdd

Premises used: HurwitzZeta.differentiable_hurwitzZetaOdd
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
rw : cosZeta a s = (cosZeta a s + I * sinZeta a s + (cosZeta a s + I * -sinZeta a s)) / 2
⊢ cosZeta a s = (expZeta a s + expZeta (-a) s) / 2

Tactic:
rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg]

Premises used: HurwitzZeta.expZeta, HurwitzZeta.sinZeta_neg, HurwitzZeta.cosZeta_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
⊢ cosZeta a s = (cosZeta a s + I * sinZeta a s + (cosZeta a s + I * -sinZeta a s)) / 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
rw : sinZeta a s = (cosZeta a s + I * sinZeta a s - (cosZeta a s + I * -sinZeta a s)) / (2 * I)
⊢ sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * I)

Tactic:
rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg]

Premises used: HurwitzZeta.expZeta, HurwitzZeta.sinZeta_neg, HurwitzZeta.cosZeta_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
⊢ sinZeta a s = (cosZeta a s + I * sinZeta a s - (cosZeta a s + I * -sinZeta a s)) / (2 * I)

Tactic:
field
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum
    (fun (b : ℕ) ↦
      (↑(Real.cos (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s +
        I * ((↑(Real.sin (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s))
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s + I * sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
(hasSum_nat_cosZeta a hs).add ((hasSum_nat_sinZeta a hs).mul_left I)

Premises used: HasSum.add, HurwitzZeta.hasSum_nat_sinZeta, HurwitzZeta.hasSum_nat_cosZeta, HasSum.mul_left, Complex.I