awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
⊢ 0 < 3 / 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (ofReal ∘ oddKernel a) (1 / x) = (1 * (↑(x ^ (3 / 2)) : ℂ)) • (ofReal ∘ sinKernel a) x

Tactic:
simp [← ofReal_mul, oddKernel_functional_equation a, inv_rpow (le_of_lt hx)]

Premises used: Real.inv_rpow, le_of_lt, HurwitzZeta.oddKernel_functional_equation, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
r : ℝ
let :
  ∀ (v : ℝ) (hv : 0 < v) (hv' : IsBigO (F := ℝ) atTop (oddKernel a) fun (x : ℝ) ↦ rexp (-v * x)),
    IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ oddKernel a) x - 0) fun (x : ℝ) ↦ x ^ r
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ oddKernel a) x - 0) fun (x : ℝ) ↦ x ^ r

Tactic:
let ⟨v, hv, hv'⟩ := isBigO_atTop_oddKernel a
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : IsBigO (F := ℝ) atTop (oddKernel a) fun (x : ℝ) ↦ rexp (-v * x)
rw :
  ∀ (hv' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖oddKernel a x‖) fun (x : ℝ) ↦ rexp (-v * x)),
    IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(ofReal ∘ oddKernel a) x - 0‖) fun (x : ℝ) ↦ x ^ r
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ oddKernel a) x - 0) fun (x : ℝ) ↦ x ^ r

Tactic:
rw [← isBigO_norm_left] at hv' ⊢

Premises used: Asymptotics.isBigO_norm_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖oddKernel a x‖) fun (x : ℝ) ↦ rexp (-v * x)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(ofReal ∘ oddKernel a) x - 0‖) fun (x : ℝ) ↦ x ^ r

Tactic:
simpa using hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO

Premises used: isLittleO_exp_neg_mul_rpow_atTop, Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
r : ℝ
let :
  ∀ (v : ℝ) (hv : 0 < v) (hv' : IsBigO (F := ℝ) atTop (sinKernel a) fun (x : ℝ) ↦ rexp (-v * x)),
    IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ sinKernel a) x - 0) fun (x : ℝ) ↦ x ^ r
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ sinKernel a) x - 0) fun (x : ℝ) ↦ x ^ r

Tactic:
let ⟨v, hv, hv'⟩ := isBigO_atTop_sinKernel a
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : IsBigO (F := ℝ) atTop (sinKernel a) fun (x : ℝ) ↦ rexp (-v * x)
rw :
  ∀ (hv' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖sinKernel a x‖) fun (x : ℝ) ↦ rexp (-v * x)),
    IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(ofReal ∘ sinKernel a) x - 0‖) fun (x : ℝ) ↦ x ^ r
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ sinKernel a) x - 0) fun (x : ℝ) ↦ x ^ r

Tactic:
rw [← isBigO_norm_left] at hv' ⊢

Premises used: Asymptotics.isBigO_norm_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖sinKernel a x‖) fun (x : ℝ) ↦ rexp (-v * x)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(ofReal ∘ sinKernel a) x - 0‖) fun (x : ℝ) ↦ x ^ r

Tactic:
simpa using hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO

Premises used: isLittleO_exp_neg_mul_rpow_atTop, Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
⊢ Differentiable ℂ (completedHurwitzZetaOdd a)

Tactic:
((hurwitzOddFEPair a).differentiable_Λ.comp
    ((differentiable_id.add_const 1).div_const 2)).div_const 2

Premises used: StrongFEPair.differentiable_Λ, HurwitzZeta.completedHurwitzZetaOdd, HurwitzZeta.hurwitzOddFEPair, StrongFEPair.Λ, Differentiable.div_const, mellin, OfNat.ofNat, Differentiable.comp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
⊢ Differentiable ℂ (completedSinZeta a)

Tactic:
((hurwitzOddFEPair a).symm.differentiable_Λ.comp
    ((differentiable_id.add_const 1).div_const 2)).div_const 2

Premises used: StrongFEPair.differentiable_Λ, HurwitzZeta.hurwitzOddFEPair, StrongFEPair.symm, HurwitzZeta.completedSinZeta, StrongFEPair.Λ, Differentiable.div_const, mellin, OfNat.ofNat, Differentiable.comp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd (-a) s = -completedHurwitzZetaOdd a s

Tactic:
simp [completedHurwitzZetaOdd, StrongFEPair.Λ, hurwitzOddFEPair, mellin, oddKernel_neg,
    integral_neg, neg_div]

Premises used: neg_div, HurwitzZeta.completedHurwitzZetaOdd, MeasureTheory.integral_neg, HurwitzZeta.hurwitzOddFEPair, StrongFEPair.Λ, HurwitzZeta.oddKernel_neg, mellin
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedSinZeta (-a) s = -completedSinZeta a s

Tactic:
simp [completedSinZeta, StrongFEPair.Λ, mellin, StrongFEPair.symm, WeakFEPair.symm,
    hurwitzOddFEPair, sinKernel_neg, integral_neg, neg_div]

Premises used: neg_div, HurwitzZeta.sinKernel_neg, MeasureTheory.integral_neg, HurwitzZeta.hurwitzOddFEPair, StrongFEPair.symm, HurwitzZeta.completedSinZeta, StrongFEPair.Λ, mellin, WeakFEPair.symm
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
push_cast : (1 - s + 1) / 2 = HDiv.hDiv (α := ℂ) 3 2 - (s + 1) / 2
⊢ (1 - s + 1) / 2 = (↑(3 / 2) : ℂ) - (s + 1) / 2

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = HDiv.hDiv (α := ℂ) 3 2 - (s + 1) / 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
ring ring₁ : (1 - s + 1) / 2 = HDiv.hDiv (α := ℂ) 3 2 - (s + 1) / 2
⊢ (1 - s + 1) / 2 = (↑(3 / 2) : ℂ) - (s + 1) / 2

Tactic:
{ push_cast; ring }
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
rw : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = completedSinZeta a s
rw₁ : (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₂ : (hurwitzOddFEPair a).Λ ((↑(3 / 2) : ℂ) - (s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₃ :
  (hurwitzOddFEPair a).Λ ((↑(hurwitzOddFEPair a).k : ℂ) - (s + 1) / 2) / 2 =
    (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₄ : UnitAddCircle
rw₅ :
  (hurwitzOddFEPair a).ε • (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₆ :
  HSMul.hSMul (α := ℂ) 1 ((hurwitzOddFEPair a).symm.Λ ((s + 1) / 2)) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
rw₇ rw₈ : (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s

Tactic:
rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]

Premises used: HurwitzZeta.completedHurwitzZetaOdd, StrongFEPair.functional_equation, HurwitzZeta.hurwitzOddFEPair, HDiv.hDiv, one_smul, HurwitzZeta.completedSinZeta, HurwitzZeta.hurwitzOddFEPair_ε, HAdd.hAdd, HurwitzZeta.hurwitzOddFEPair_k, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedSinZeta a (1 - s) = completedHurwitzZetaOdd a s

Tactic:
simp [← completedHurwitzZetaOdd_one_sub]

Premises used: HurwitzZeta.completedHurwitzZetaOdd_one_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
push_cast : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = (↑(2 * π * a * (↑n : ℝ)) : ℂ) * I

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
ring ring₁ : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = (↑(2 * π * a * (↑n : ℝ)) : ℂ) * I

Tactic:
{ push_cast; ring }
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
n : ℤ
simp_rw : ‖-I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2‖ = 1 / 2
simp_rw₁ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) / 2‖ = 1 / 2
simp_rw₂ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / Norm.norm (E := ℂ) 2 = 1 / 2
simp_rw₃ : ‖-I * cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₄ : ‖-I‖ * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₅ : ‖I‖ * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₆ : 1 * ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
simp_rw₇ : ‖cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)‖ / 2 = 1 / 2
⊢ ‖c n‖ = 1 / 2

Tactic:
simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]

Premises used: RCLike.norm_ofNat, norm_mul, norm_div, norm_neg, Complex.norm_I, Complex.norm_exp_ofReal_mul_I, one_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
⊢ ∀ (n : ℤ), ‖c n‖ = 1 / 2

Tactic:
have hc (n : ℤ) : ‖c n‖ = 1 / 2 := by
    simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
⊢ HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)

Tactic:
((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HasSum.div_const, HurwitzZeta.hasSum_int_sinKernel, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
refine :
  ∀ (n : ℤ),
    c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
      -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
        2
⊢ HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)

Tactic:
refine ((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HasSum.div_const, HurwitzZeta.hasSum_int_sinKernel, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
n : ℤ
rw :
  -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑n : ℂ) / 2 *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
rw₁ :
  -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑n : ℂ) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2 =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
rw₂ rw₃ :
  -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2 =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
⊢ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2

Tactic:
rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]

Premises used: div_mul_eq_mul_div, mul_right_comm, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
⊢ ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)

Tactic:
have hF t (ht : 0 < t) :
      HasSum (fun n ↦ c n * n * rexp (-π * n ^ 2 * t)) (sinKernel a t / 2) := by
    refine ((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_
    rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
simp_rw : Summable (α := ℝ) fun (i : ℤ) ↦ 1 / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re / 2
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re

Tactic:
simp_rw [hc, div_right_comm]

Premises used: div_right_comm
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h : Summable (α := ℝ) fun (i : ℤ) ↦ 1 / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ 1 / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re / 2

Tactic:
apply Summable.div_const

Premises used: Summable.div_const
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| s.re
h₁ : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) |(↑(-(↑n : ℤ)) : ℝ)| s.re
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ 1 / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re

Tactic:
apply Summable.of_nat_of_neg

Premises used: Summable.of_nat_of_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| s.re

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) |(↑(-(↑n : ℤ)) : ℝ)| s.re

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re

Tactic:
have h_sum : Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re := by
    simp_rw [hc, div_right_comm]
    apply Summable.div_const
    apply Summable.of_nat_of_neg <;>
    simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
refine :
  ∀ (n : ℤ),
    (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
          HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
        2 =
      (s + 1).Gammaℝ * c n * (↑((SignType.sign : (a : ℝ) → SignType) (↑n : ℝ)) : ℂ) / (↑|(↑n : ℝ)| : ℂ) ^ s
⊢ HasSum
    (fun (n : ℤ) ↦
      (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
          HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
refine (mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum).congr_fun
    fun n ↦ ?_
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
n : ℤ
simp :
  -((s + 1).Gammaℝ * I * (↑((SignType.sign : (a : ℤ) → SignType) n) : ℂ) *
            cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
        HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
      2 =
    (s + 1).Gammaℝ * c n * (↑((SignType.sign : (a : ℤ) → SignType) n) : ℂ) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s
⊢ (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
        HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
      2 =
    (s + 1).Gammaℝ * c n * (↑((SignType.sign : (a : ℝ) → SignType) (↑n : ℝ)) : ℂ) / (↑|(↑n : ℝ)| : ℂ) ^ s

Tactic:
simp [Int.sign_eq_sign, ← Int.cast_abs]

Premises used: Int.cast_abs, Int.sign_eq_sign
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
n : ℤ
⊢ -((s + 1).Gammaℝ * I * (↑((SignType.sign : (a : ℤ) → SignType) n) : ℂ) *
            cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
        HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
      2 =
    (s + 1).Gammaℝ * c n * (↑((SignType.sign : (a : ℤ) → SignType) n) : ℂ) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum
    (fun (n : ℕ) ↦
      (s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) /
            HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s /
          2 +
        (s + 1).Gammaℝ * -I * (↑(Int.sign (-(↑n : ℤ))) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) /
            HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s +
      (s + 1).Gammaℝ * -I * (↑(Int.sign 0) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) /
          HPow.hPow (α := ℂ) (↑|0| : ℂ) s /
        2)

Tactic:
have := (hasSum_int_completedSinZeta a hs).nat_add_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      (s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) /
            HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s /
          2 +
        (s + 1).Gammaℝ * -I * (↑(Int.sign (-(↑n : ℤ))) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) /
            HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s +
      (s + 1).Gammaℝ * -I * (↑(Int.sign 0) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) /
          HPow.hPow (α := ℂ) (↑|0| : ℂ) s /
        2)
⊢ HasSum
    (fun (n : ℕ) ↦
      ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
            (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
simp_rw [Int.sign_zero, Int.cast_zero, mul_zero, zero_mul, zero_div, add_zero, abs_neg,
    Int.sign_neg, Nat.abs_cast, Int.cast_neg, Int.cast_natCast, ← add_div] at this

Premises used: Int.cast_neg, Int.cast_natCast, abs_neg, Nat.abs_cast, Int.cast_zero, MulZeroClass.zero_mul, zero_div, MulZeroClass.mul_zero, Int.sign_zero, Int.sign_neg, add_zero, add_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
            (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
⊢ HasSum (fun (n : ℕ) ↦ (s + 1).Gammaℝ * (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
this.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun