awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
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
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 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

Premises used: HurwitzZeta.completedHurwitzZetaEven₀, HDiv.hDiv, OfNat.ofNat, ite
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
e_a₅ e_a₆ :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / 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

Tactic:
rw [smul_eq_mul, mul_comm, mul_div_assoc, div_div, div_mul_cancel₀ _ two_ne_zero, mul_one_div]

Premises used: div_mul_cancel₀, mul_div_assoc, two_ne_zero, mul_one_div, mul_comm, smul_eq_mul, div_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
e_a : HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) 1 / 2 = 1 / (1 - s)
⊢ HSMul.hSMul (β := ℂ) (1 / ((↑(1 / 2) : ℂ) - s / 2)) 1 / 2 = 1 / (1 - s)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
e_a₄ e_a₅ : 1 / (1 - s) = 1 / (1 - s)
⊢ HSMul.hSMul (β := ℂ) (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]

Premises used: div_mul_cancel₀, sub_div, two_ne_zero, smul_eq_mul, div_div, mul_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
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)
⊢ completedCosZeta a s = completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s)

Tactic:
rw [completedCosZeta, WeakFEPair.Λ, sub_div, sub_div]

Premises used: WeakFEPair.Λ, sub_div, HurwitzZeta.completedCosZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
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)
⊢ (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:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  ((hurwitzEvenFEPair a).ε⁻¹ / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₁ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / ((↑(1 / 2) : ℂ) - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₂ :
  HSMul.hSMul (β := ℂ) (1⁻¹ / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₃ :
  HSMul.hSMul (β := ℂ) (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) (if a = 0 then 1 else 0) / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
e_a₄ : (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) * if a = 0 then 1 else 0) / 2 = (if a = 0 then 1 else 0) / (1 - s)
e_a₅ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2)) / 2 = (if a = 0 then 1 else 0) / (1 - s)
e_a₆ : (if a = 0 then 1 else 0) * (1 / (HDiv.hDiv (α := ℂ) 1 2 - s / 2) / 2) = (if a = 0 then 1 else 0) / (1 - s)
e_a₇ : (if a = 0 then 1 else 0) * (1 / ((HDiv.hDiv (α := ℂ) 1 2 - s / 2) * 2)) = (if a = 0 then 1 else 0) / (1 - s)
e_a₈ : (if a = 0 then 1 else 0) * (1 / ((1 - s) / 2 * 2)) = (if a = 0 then 1 else 0) / (1 - s)
e_a₉ : (if a = 0 then 1 else 0) * (1 / (1 - s)) = (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)

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]

Premises used: div_mul_cancel₀, inv_one, mul_div_assoc, sub_div, two_ne_zero', mul_one_div, mul_comm, smul_eq_mul, div_div, Complex, WeakFEPair.symm, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven (-a) s = completedHurwitzZetaEven a s

Tactic:
simp [completedHurwitzZetaEven]

Premises used: HurwitzZeta.completedHurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ (-a) s = completedHurwitzZetaEven₀ a s

Tactic:
simp [completedHurwitzZetaEven₀]

Premises used: HurwitzZeta.completedHurwitzZetaEven₀
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedCosZeta (-a) s = completedCosZeta a s

Tactic:
simp [completedCosZeta]

Premises used: HurwitzZeta.completedCosZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedCosZeta₀ (-a) s = completedCosZeta₀ a s

Tactic:
simp [completedCosZeta₀]

Premises used: HurwitzZeta.completedCosZeta₀
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
⊢ 1 / 2 = (↑(1 / 2) : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
⊢ 1 / 2 = (hurwitzEvenFEPair a).k

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).ε = 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = completedCosZeta a s
rw₁ : (hurwitzEvenFEPair a).Λ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₄ : (hurwitzEvenFEPair a).Λ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₅ : (hurwitzEvenFEPair a).ε • (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₆ : HSMul.hSMul (α := ℂ) 1 ((hurwitzEvenFEPair a).symm.Λ (s / 2)) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
rw₇ rw₈ : (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s

Tactic:
rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]

Premises used: HDiv.hDiv, sub_div, one_smul, WeakFEPair.functional_equation, HurwitzZeta.completedHurwitzZetaEven, OfNat.ofNat, HurwitzZeta.completedCosZeta, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
rw₁ : (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₂ : (hurwitzEvenFEPair a).Λ₀ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₃ : (hurwitzEvenFEPair a).Λ₀ ((↑(1 / 2) : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₄ : (hurwitzEvenFEPair a).Λ₀ ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₅ : (hurwitzEvenFEPair a).ε • (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₆ : HSMul.hSMul (α := ℂ) 1 ((hurwitzEvenFEPair a).symm.Λ₀ (s / 2)) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
rw₇ rw₈ : (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s

Tactic:
rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]

Premises used: HurwitzZeta.completedHurwitzZetaEven₀, HDiv.hDiv, HurwitzZeta.completedCosZeta₀, sub_div, one_smul, WeakFEPair.functional_equation₀, OfNat.ofNat, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
rw : completedHurwitzZetaEven a (1 - (1 - s)) = completedHurwitzZetaEven a s
rw₁ rw₂ : completedHurwitzZetaEven a s = completedHurwitzZetaEven a s
⊢ completedCosZeta a (1 - s) = completedHurwitzZetaEven a s

Tactic:
rw [← completedHurwitzZetaEven_one_sub, sub_sub_cancel]

Premises used: HurwitzZeta.completedHurwitzZetaEven_one_sub, sub_sub_cancel
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
rw : completedHurwitzZetaEven₀ a (1 - (1 - s)) = completedHurwitzZetaEven₀ a s
rw₁ rw₂ : completedHurwitzZetaEven₀ a s = completedHurwitzZetaEven₀ a s
⊢ completedCosZeta₀ a (1 - s) = completedHurwitzZetaEven₀ a s

Tactic:
rw [← completedHurwitzZetaEven₀_one_sub, sub_sub_cancel]

Premises used: sub_sub_cancel, HurwitzZeta.completedHurwitzZetaEven₀_one_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven a) s

Tactic:
(((hurwitzEvenFEPair a).differentiableAt_Λ ?_ (Or.inl ?_)).comp s
      (differentiableAt_id.div_const _)).div_const _

Premises used: WeakFEPair.differentiableAt_Λ, WeakFEPair.Λ, HurwitzZeta.completedHurwitzZetaEven, DifferentiableAt.comp, Or.inl, DifferentiableAt.div_const, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
refine_1 : s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
refine_2 : s / 2 ≠ (↑(hurwitzEvenFEPair a).k : ℂ)
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven a) s

Tactic:
refine (((hurwitzEvenFEPair a).differentiableAt_Λ ?_ (Or.inl ?_)).comp s
      (differentiableAt_id.div_const _)).div_const _

Premises used: WeakFEPair.differentiableAt_Λ, DifferentiableAt.comp, Or.inl, DifferentiableAt.div_const, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
refine_1 : ∀ (h : s ≠ 0), s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
refine_1₁ : ∀ (h : a ≠ 0), s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0

Tactic:
rcases hs with h | h
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
h : s ≠ 0
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0

Tactic:
simp [hurwitzEvenFEPair, h]

Premises used: HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
h : a ≠ 0
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0

Tactic:
simp [hurwitzEvenFEPair, h]

Premises used: HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
refine_2 : s / 2 ≠ HDiv.hDiv (α := ℂ) 1 2
⊢ s / 2 ≠ (↑(1 / 2) : ℂ)

Tactic:
rw [ofReal_div, ofReal_one, ofReal_ofNat]

Premises used: Complex.ofReal_one, Complex.ofReal_div, Complex.ofReal_ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ HDiv.hDiv (α := ℂ) 1 2

Tactic:
hs' ∘ (div_left_inj' two_ne_zero).mp

Premises used: Function.comp, two_ne_zero, Iff.mp, div_left_inj', Not
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ HDiv.hDiv (α := ℂ) 1 2

Tactic:
exact hs' ∘ (div_left_inj' two_ne_zero).mp

Premises used: two_ne_zero, Iff.mp, div_left_inj'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ Differentiable ℂ (completedHurwitzZetaEven₀ a)

Tactic:
((hurwitzEvenFEPair a).differentiable_Λ₀.comp (differentiable_id.div_const _)).div_const _

Premises used: HurwitzZeta.completedHurwitzZetaEven₀, WeakFEPair.Λ₀, Differentiable.div_const, mellin, Differentiable.comp, HurwitzZeta.hurwitzEvenFEPair, WeakFEPair.differentiable_Λ₀
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
s : ℂ
simp_rw :
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s) -
      (completedHurwitzZetaEven₀ b s - (if b = 0 then 1 else 0) / s - 1 / (1 - s)) =
    completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
      ((if a = 0 then 1 else 0) / s - (if b = 0 then 1 else 0) / s)
⊢ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
    completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
      HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s

Tactic:
simp_rw [completedHurwitzZetaEven_eq, sub_div]

Premises used: HurwitzZeta.completedHurwitzZetaEven_eq, sub_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s) -
      (completedHurwitzZetaEven₀ b s - (if b = 0 then 1 else 0) / s - 1 / (1 - s)) =
    completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
      ((if a = 0 then 1 else 0) / s - (if b = 0 then 1 else 0) / s)

Tactic:
abel
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
⊢ ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s

Tactic:
have (s : _) : completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
      ((if a = 0 then 1 else 0) - (if b = 0 then 1 else 0)) / s := by
    simp_rw [completedHurwitzZetaEven_eq, sub_div]
    abel
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
rw :
  DifferentiableAt ℂ (F := ℂ)
    (fun (x : ℂ) ↦
      completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / x)
    1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1

Tactic:
rw [funext this]

Premises used: funext
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (x : ℂ) ↦
      completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / x)
    1

Tactic:
.sub ?_ <| (differentiable_const _ _).div (differentiable_id _) one_ne_zero

Premises used: DifferentiableAt.div, differentiable_const, DifferentiableAt.sub, differentiable_id, one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
refine : DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x) 1
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (x : ℂ) ↦
      completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / x)
    1

Tactic:
refine .sub ?_ <| (differentiable_const _ _).div (differentiable_id _) one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
hf : DifferentiableAt ℂ (completedHurwitzZetaEven₀ a) 1
hg : DifferentiableAt ℂ (completedHurwitzZetaEven₀ b) 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x) 1

Tactic:
apply DifferentiableAt.sub

Premises used: DifferentiableAt.sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven₀ a) 1

Tactic:
apply differentiable_completedHurwitzZetaEven₀

Premises used: HurwitzZeta.differentiable_completedHurwitzZetaEven₀
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven₀ b) 1

Tactic:
apply differentiable_completedHurwitzZetaEven₀

Premises used: HurwitzZeta.differentiable_completedHurwitzZetaEven₀
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (completedCosZeta a) s

Tactic:
(((hurwitzEvenFEPair a).symm.differentiableAt_Λ (Or.inl ?_) ?_).comp s
      (differentiableAt_id.div_const _)).div_const _

Premises used: WeakFEPair.differentiableAt_Λ, WeakFEPair.Λ, DifferentiableAt.comp, Or.inl, DifferentiableAt.div_const, WeakFEPair.symm, HurwitzZeta.completedCosZeta, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
refine_1 : s / 2 ≠ 0
refine_2 : s / 2 ≠ (↑(hurwitzEvenFEPair a).symm.k : ℂ) ∨ (hurwitzEvenFEPair a).symm.g₀ = 0
⊢ DifferentiableAt ℂ (completedCosZeta a) s

Tactic:
refine (((hurwitzEvenFEPair a).symm.differentiableAt_Λ (Or.inl ?_) ?_).comp s
      (differentiableAt_id.div_const _)).div_const _

Premises used: WeakFEPair.differentiableAt_Λ, DifferentiableAt.comp, Or.inl, DifferentiableAt.div_const, WeakFEPair.symm, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ 0

Tactic:
div_ne_zero_iff.mpr ⟨hs, two_ne_zero⟩

Premises used: Iff.mpr, div_ne_zero_iff, two_ne_zero, And.intro
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ 0

Tactic:
exact div_ne_zero_iff.mpr ⟨hs, two_ne_zero⟩

Premises used: Iff.mpr, div_ne_zero_iff, two_ne_zero, And.intro
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
refine_2 : s / 2 ≠ (↑(1 / 2) : ℂ) ∨ Eq (α := ℂ) (if a = 0 then 1 else 0) 0
⊢ s / 2 ≠ (↑(hurwitzEvenFEPair a).symm.k : ℂ) ∨ (hurwitzEvenFEPair a).symm.g₀ = 0

Tactic:
change s / 2 ≠ ↑(1 / 2 : ℝ) ∨ (if a = 0 then 1 else 0) = 0

Premises used: HDiv.hDiv, OfNat.ofNat, ite
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ (↑(1 / 2) : ℂ) ∨ Eq (α := ℂ) (if a = 0 then 1 else 0) 0

Tactic:
Or.imp (fun h ↦ ?_) (fun ha ↦ ?_) hs'

Premises used: Or.imp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
refine_2 : ∀ (h : s ≠ 1), s / 2 ≠ (↑(1 / 2) : ℂ)
refine_2₁ : ∀ (ha : a ≠ 0), Eq (α := ℂ) (if a = 0 then 1 else 0) 0
⊢ s / 2 ≠ (↑(1 / 2) : ℂ) ∨ Eq (α := ℂ) (if a = 0 then 1 else 0) 0

Tactic:
refine Or.imp (fun h ↦ ?_) (fun ha ↦ ?_) hs'

Premises used: Or.imp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
h : s ≠ 1
⊢ s / 2 ≠ (↑(1 / 2) : ℂ)

Tactic:
simpa [push_cast] using h ∘ (div_left_inj' two_ne_zero).mp

Premises used: two_ne_zero, Iff.mp, div_left_inj'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
ha : a ≠ 0
⊢ Eq (α := ℂ) (if a = 0 then 1 else 0) 0

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ Differentiable ℂ (completedCosZeta₀ a)

Tactic:
((hurwitzEvenFEPair a).symm.differentiable_Λ₀.comp (differentiable_id.div_const _)).div_const _

Premises used: WeakFEPair.Λ₀, HurwitzZeta.completedCosZeta₀, Differentiable.div_const, mellin, WeakFEPair.symm, Differentiable.comp, HurwitzZeta.hurwitzEvenFEPair, WeakFEPair.differentiable_Λ₀
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℂ
⊢ Tendsto (fun (s : ℂ) ↦ s / 2) (𝓝[≠] a) (𝓝[≠] (a / 2))

Tactic:
le_of_eq ((Homeomorph.mulRight₀ _ (inv_ne_zero (two_ne_zero' ℂ))).map_punctured_nhds_eq a)

Premises used: Homeomorph.map_punctured_nhds_eq, Homeomorph.mulRight₀, two_ne_zero', Filter.Tendsto, inv_ne_zero, Complex, le_of_eq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ Tendsto (fun (s : ℂ) ↦ (s - (↑(1 / 2) : ℂ)) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (↑(1 / 2) : ℂ))
    (𝓝 (HMul.hMul (α := ℂ) 1 1))

Tactic:
have h1 : Tendsto (fun s : ℂ ↦ (s - ↑(1 / 2 : ℝ)) * _) (𝓝[≠] ↑(1 / 2 : ℝ))
    (𝓝 ((1 : ℂ) * (1 : ℂ))) := (hurwitzEvenFEPair a).Λ_residue_k
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 :
  Tendsto (fun (s : ℂ) ↦ (s - (↑(1 / 2) : ℂ)) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (↑(1 / 2) : ℂ))
    (𝓝 (HMul.hMul (α := ℂ) 1 1))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s)
    (𝓝[≠] HDiv.hDiv (α := ℂ) 1 2) (𝓝 1)

Tactic:
simp only [push_cast, one_mul] at h1

Premises used: one_mul