awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
inr :
  1 / (-I * τ) ^ (3 / 2) *
      (-I * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
        (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (3 / 2) * (-2 * (↑π : ℂ) * jacobiTheta₂'' z (-1 / τ))
⊢ jacobiTheta₂' z τ = -2 * (↑π : ℂ) / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)

Tactic:
rw [jacobiTheta₂'_functional_equation, ← mul_one_div _ τ, mul_right_comm _ (cexp _),
    (by rw [cpow_one, ← div_div, div_self (neg_ne_zero.mpr I_ne_zero)] :
      1 / τ = -I / (-I * τ) ^ (1 : ℂ)), div_mul_div_comm,
    ← cpow_add _ _ (mul_ne_zero (neg_ne_zero.mpr I_ne_zero) hτ), ← div_mul_eq_mul_div,
    (by norm_num : (1 / 2 + 1 : ℂ) = 3 / 2), mul_assoc (1 / _), mul_assoc (1 / _),
    ← mul_one_div (-2 * π : ℂ), mul_comm _ (1 / _), mul_assoc (1 / _)]

Premises used: Iff.mpr, Real.pi, HMul.hMul, div_mul_div_comm, mul_assoc, HDiv.hDiv, Complex.I_ne_zero, div_mul_eq_mul_div, Complex.ofReal, jacobiTheta₂'_functional_equation, mul_one_div, mul_right_comm, Complex.cpow_add, mul_comm, Complex.exp, neg_ne_zero, mul_ne_zero, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
inr :
  -I * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
    -2 * (↑π : ℂ) * jacobiTheta₂'' z (-1 / τ)
⊢ 1 / (-I * τ) ^ (3 / 2) *
      (-I * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
        (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (3 / 2) * (-2 * (↑π : ℂ) * jacobiTheta₂'' z (-1 / τ))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
inr :
  I *
      (cexp (-((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) *
        -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) =
    I *
      (cexp (-((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)))
⊢ -I * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
    -2 * (↑π : ℂ) * jacobiTheta₂'' z (-1 / τ)

Tactic:
rw [jacobiTheta₂'', div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc, ← mul_div_assoc,
    ← div_mul_eq_mul_div (-2 * π : ℂ), mul_assoc, aux1, mul_div z (-1), mul_neg_one, neg_div τ z,
    jacobiTheta₂_neg_left, jacobiTheta₂'_neg_left, neg_mul, ← mul_neg, ← mul_neg,
    mul_div, mul_neg_one, neg_div, neg_mul, neg_mul, neg_div]

Premises used: mul_div, neg_div, Real.pi, HMul.hMul, Complex.two_pi_I_ne_zero, jacobiTheta₂_neg_left, mul_assoc, mul_div_assoc, HurwitzZeta.jacobiTheta₂'', div_add', div_mul_eq_mul_div, jacobiTheta₂'_neg_left, Complex.ofReal, neg_mul, mul_neg_one, OfNat.ofNat, Neg.neg, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
inr :
  -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
⊢ I *
      (cexp (-((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) *
        -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) =
    I *
      (cexp (-((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)))

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
inr :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
inr₁ :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I) - jacobiTheta₂' (z / τ) (-(1 / τ))
inr₂ :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    2 * (↑π : ℂ) * I * (z * jacobiTheta₂ (z / τ) (-(1 / τ))) - jacobiTheta₂' (z / τ) (-(1 / τ))
inr₃ inr₄ :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ))
⊢ -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)

Tactic:
rw [neg_sub, ← sub_eq_neg_add, mul_comm _ (_ * I), ← mul_assoc]

Premises used: neg_sub, HMul.hMul, sub_eq_neg_add, mul_assoc, mul_comm, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
⊢ Function.Periodic (β := ℝ) (fun (a : ℝ) ↦ (jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ))).re) 1

Tactic:
simp [jacobiTheta₂''_add_left]

Premises used: HurwitzZeta.jacobiTheta₂''_add_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
⊢ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) = jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ))

Tactic:
simp [oddKernel, ← conj_eq_iff_re, jacobiTheta₂''_conj]

Premises used: HurwitzZeta.oddKernel, Complex.conj_eq_iff_re, HurwitzZeta.jacobiTheta₂''_conj
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
⊢ (↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ)) =
    HPow.hPow (β := ℕ) I 2 * (↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : x ≤ 0
a' : ℝ
H H₁ : (I * (↑x : ℂ)).im ≤ 0
⊢ oddKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0

Tactic:
rw [← ofReal_eq_zero, oddKernel_def', jacobiTheta₂_undef, jacobiTheta₂'_undef, zero_div, zero_add,
    mul_zero, mul_zero]

Premises used: HurwitzZeta.oddKernel_def', zero_div, zero_add, MulZeroClass.mul_zero, Complex.ofReal_eq_zero, jacobiTheta₂_undef, jacobiTheta₂'_undef
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * (↑x : ℂ)).im ≤ 0

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
H : ∀ (a' : ℝ), oddKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
⊢ oddKernel a x = 0

Tactic:
induction a using QuotientAddGroup.induction_on with | H a' =>
  rw [← ofReal_eq_zero, oddKernel_def', jacobiTheta₂_undef, jacobiTheta₂'_undef, zero_div, zero_add,
    mul_zero, mul_zero] <;>
  simpa

Premises used: HurwitzZeta.oddKernel_def', zero_div, zero_add, MulZeroClass.mul_zero, Complex.ofReal_eq_zero, jacobiTheta₂_undef, jacobiTheta₂'_undef
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
⊢ Function.Periodic (β := ℝ) (fun (ξ : ℝ) ↦ (jacobiTheta₂' (↑ξ : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ))).re) 1

Tactic:
simp [jacobiTheta₂'_add_left]

Premises used: jacobiTheta₂'_add_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
⊢ (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) = jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ))

Tactic:
simp [sinKernel, re_eq_add_conj, jacobiTheta₂'_conj, map_ofNat]

Premises used: Complex.re_eq_add_conj, jacobiTheta₂'_conj, map_ofNat, HurwitzZeta.sinKernel
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : x ≤ 0
a : ℝ
⊢ (I * (↑x : ℂ)).im ≤ 0

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : x ≤ 0
a : ℝ
H : (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) = 0
H₁ : jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ)) = 0
H₂ : 0 / (-2 * (↑π : ℂ)) = 0
H₃ H₄ : Eq (α := ℂ) 0 0
⊢ sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0

Tactic:
rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]

Premises used: zero_div, Complex.ofReal_eq_zero, jacobiTheta₂'_undef, HurwitzZeta.sinKernel_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
H : ∀ (a : ℝ), sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
⊢ sinKernel a x = 0

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H a => rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]

Premises used: zero_div, Complex.ofReal_eq_zero, jacobiTheta₂'_undef, HurwitzZeta.sinKernel_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x a : ℝ
⊢ oddKernel (-(↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) x = -oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x

Tactic:
simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, oddKernel_def, jacobiTheta₂''_neg_left]

Premises used: HurwitzZeta.jacobiTheta₂''_neg_left, HurwitzZeta.oddKernel_def, Complex.ofReal_inj, QuotientAddGroup.mk_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
H : ∀ (a : ℝ), oddKernel (-(↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) x = -oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x
⊢ oddKernel (-a) x = -oddKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H a => simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, oddKernel_def, jacobiTheta₂''_neg_left]

Premises used: HurwitzZeta.jacobiTheta₂''_neg_left, HurwitzZeta.oddKernel_def, Complex.ofReal_inj, QuotientAddGroup.mk_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
⊢ oddKernel 0 x = 0

Tactic:
simpa using oddKernel_neg 0 x

Premises used: HurwitzZeta.oddKernel_neg, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x a : ℝ
⊢ sinKernel (-(↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) x = -sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x

Tactic:
simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, sinKernel_def, jacobiTheta₂'_neg_left,
      neg_div]

Premises used: neg_div, jacobiTheta₂'_neg_left, Complex.ofReal_inj, HurwitzZeta.sinKernel_def, QuotientAddGroup.mk_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
H : ∀ (a : ℝ), sinKernel (-(↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) x = -sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x
⊢ sinKernel (-a) x = -sinKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H a => simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, sinKernel_def, jacobiTheta₂'_neg_left,
      neg_div]

Premises used: neg_div, jacobiTheta₂'_neg_left, Complex.ofReal_inj, HurwitzZeta.sinKernel_def, QuotientAddGroup.mk_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
⊢ sinKernel 0 x = 0

Tactic:
simpa using sinKernel_neg 0 x

Premises used: HurwitzZeta.sinKernel_neg, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
⊢ ContinuousOn (oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)

Tactic:
suffices ContinuousOn (fun x ↦ (oddKernel a x : ℂ)) (Ioi 0) from
    (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
H :
  ContinuousOn (Y := ℂ)
    (fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
        (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
          (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))))
    (Ioi 0)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)

Tactic:
simp_rw [oddKernel_def' a]

Premises used: HurwitzZeta.oddKernel_def'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
⊢ ContinuousOn (Y := ℂ)
    (fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
        (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
          (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))))
    (Ioi 0)

Tactic:
fun x hx ↦ ((Continuous.continuousAt ?_).mul ?_).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, Continuous.continuousAt, ContinuousAt.mul, ContinuousOn
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
H :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
H₁ :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    ContinuousAt (Y := ℂ)
      (fun (x : ℝ) ↦
        jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
          (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
      x
⊢ ContinuousOn (Y := ℂ)
    (fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
        (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
          (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))))
    (Ioi 0)

Tactic:
refine fun x hx ↦ ((Continuous.continuousAt ?_).mul ?_).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, Continuous.continuousAt, ContinuousAt.mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Continuous (Y := ℂ × ℂ) fun (u : ℝ) ↦ ((↑a : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Continuous (Y := ℂ × ℂ) fun (u : ℝ) ↦ ((↑a : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))

Tactic:
have hf : Continuous fun u : ℝ ↦ (a * I * u, I * u) := by fun_prop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hf : Continuous (Y := ℂ × ℂ) fun (u : ℝ) ↦ ((↑a : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))
H : ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I)) x
H₁ : ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) x
⊢ ContinuousAt (Y := ℂ)
    (fun (x : ℝ) ↦
      jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    x

Tactic:
apply ContinuousAt.add

Premises used: ContinuousAt.add
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hf : Continuous (Y := ℂ × ℂ) fun (u : ℝ) ↦ ((↑a : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))
rwa : 0 < (↑x : ℂ).re
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < x
⊢ 0 < (I * (↑x : ℂ)).im

Tactic:
rwa [I_mul_im, ofReal_re]

Premises used: Complex.ofReal_re, Complex.I_mul_im
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hf : Continuous (Y := ℂ × ℂ) fun (u : ℝ) ↦ ((↑a : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I)) x

Tactic:
exact ((continuousAt_jacobiTheta₂' (a * I * x) (by rwa [I_mul_im, ofReal_re])).comp
        (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt).div_const _

Premises used: HMul.hMul, Complex.ofReal, Continuous.continuousAt, ContinuousAt.div_const, ContinuousAt.comp, continuousAt_jacobiTheta₂', Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hf : Continuous (Y := ℂ × ℂ) fun (u : ℝ) ↦ ((↑a : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) x

Tactic:
exact continuousAt_const.mul <| (continuousAt_jacobiTheta₂ (a * I * x)
        (by rwa [I_mul_im, ofReal_re])).comp (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt

Premises used: HMul.hMul, continuousAt_const, Complex.ofReal, Continuous.continuousAt, continuousAt_jacobiTheta₂, ContinuousAt.mul, ContinuousAt.comp, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
H : ∀ (a : ℝ), ContinuousOn (oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
⊢ ContinuousOn (oddKernel a) (Ioi 0)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a =>
  suffices ContinuousOn (fun x ↦ (oddKernel a x : ℂ)) (Ioi 0) from
    (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
  simp_rw [oddKernel_def' a]
  refine fun x hx ↦ ((Continuous.continuousAt ?_).mul ?_).continuousWithinAt
  · fun_prop
  · have hf : Continuous fun u : ℝ ↦ (a * I * u, I * u) := by fun_prop
    apply ContinuousAt.add
    · exact ((continuousAt_jacobiTheta₂' (a * I * x) (by rwa [I_mul_im, ofReal_re])).comp
        (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt).div_const _
    · exact continuousAt_const.mul <| (continuousAt_jacobiTheta₂ (a * I * x)
        (by rwa [I_mul_im, ofReal_re])).comp (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt

Premises used: ContinuousAt.add, ContinuousAt.continuousWithinAt, continuousAt_const, Continuous.continuousAt, ContinuousAt.mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
⊢ ContinuousOn (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)

Tactic:
suffices ContinuousOn (fun x ↦ (sinKernel a x : ℂ)) (Ioi 0) from
    (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ))) (Ioi 0)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)

Tactic:
simp_rw [sinKernel_def]

Premises used: HurwitzZeta.sinKernel_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
apply :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ))) x
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ))) (Ioi 0)

Tactic:
apply (continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)).div_const

Premises used: ContinuousOn.div_const, continuousOn_of_forall_continuousAt
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rwa : 0 < (↑x : ℂ).re
rwa₁ : ℂ
rwa₂ : 0 < x
rwa₃ : ℝ
rwa₄ : 0 < x
rwa₅ : ℝ
rwa₆ : 0 < x
rwa₇ : ℝ
rwa₈ : 0 < x
rwa₉ : ℝ
⊢ 0 < (I * (↑x : ℂ)).im

Tactic:
rwa [I_mul_im, ofReal_re]

Premises used: Complex.ofReal_re, Complex.I_mul_im
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) ((↑a : ℂ), I * (↑x : ℂ))

Tactic:
have h := continuousAt_jacobiTheta₂' a (by rwa [I_mul_im, ofReal_re])
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
h : ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ jacobiTheta₂' p.1 p.2) ((↑a : ℂ), I * (↑x : ℂ))
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ))) x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
H : ∀ (a : ℝ), ContinuousOn (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
⊢ ContinuousOn (sinKernel a) (Ioi 0)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a =>
  suffices ContinuousOn (fun x ↦ (sinKernel a x : ℂ)) (Ioi 0) from
    (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
  simp_rw [sinKernel_def]
  apply (continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)).div_const
  have h := continuousAt_jacobiTheta₂' a (by rwa [I_mul_im, ofReal_re])
  fun_prop

Premises used: ContinuousOn.div_const, continuousOn_of_forall_continuousAt, HurwitzZeta.sinKernel_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
inl : ∀ (hx : x ≤ 0), oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
inr : ∀ (hx : 0 < x), oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)

Tactic:
rcases le_or_gt x 0 with hx | hx

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
inl : 0 = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
inl₁ : 0 = 1 / x ^ (3 / 2) * 0
inl₂ inl₃ : Eq (α := ℝ) 0 0
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)

Tactic:
rw [oddKernel_undef _ hx, sinKernel_undef _ (one_div_nonpos.mpr hx), mul_zero]

Premises used: Iff.mpr, MulZeroClass.mul_zero, HurwitzZeta.sinKernel_undef, one_div_nonpos, HurwitzZeta.oddKernel_undef
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : 0 < x
a : ℝ
rw : -1 / (I * (↑x⁻¹ : ℂ)) = I * (↑x : ℂ)
rw₁ : -1 / (I * (↑x : ℂ)⁻¹) = I * (↑x : ℂ)
rw₂ : -1 / ((↑x : ℂ)⁻¹ * I) = I * (↑x : ℂ)
rw₃ : -1 / (↑x : ℂ)⁻¹ / I = I * (↑x : ℂ)
rw₄ : -1 * (↑x : ℂ) / I = I * (↑x : ℂ)
rw₅ : -1 * (↑x : ℂ) * I⁻¹ = I * (↑x : ℂ)
rw₆ : -1 * (↑x : ℂ) * -I = I * (↑x : ℂ)
rw₇ : -(-1 * (↑x : ℂ) * I) = I * (↑x : ℂ)
rw₈ : -(-(↑x : ℂ) * I) = I * (↑x : ℂ)
rw₉ : - -((↑x : ℂ) * I) = I * (↑x : ℂ)
rw₁₀ : (↑x : ℂ) * I = I * (↑x : ℂ)
rw₁₁ rw₁₂ : I * (↑x : ℂ) = I * (↑x : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)

Tactic:
rw [one_div, ofReal_inv, mul_comm, ← div_div,
    div_inv_eq_mul, div_eq_mul_inv, inv_I, mul_neg, neg_one_mul, neg_mul, neg_neg, mul_comm]

Premises used: Complex.inv_I, neg_one_mul, neg_neg, div_eq_mul_inv, one_div, mul_comm, div_inv_eq_mul, neg_mul, div_div, Complex.ofReal_inv, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)

Tactic:
have h1 : -1 / (I * ↑(1 / x)) = I * x := by rw [one_div, ofReal_inv, mul_comm, ← div_div,
    div_inv_eq_mul, div_eq_mul_inv, inv_I, mul_neg, neg_one_mul, neg_mul, neg_neg, mul_comm]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
rw : -I * I * (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
rw₁ : -(I * I) * (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
rw₂ : - -1 * (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
rw₃ : 1 * (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
rw₄ : (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
rw₅ : (↑1 : ℂ) / (↑x : ℂ) = 1 / (↑x : ℂ)
rw₆ rw₇ : 1 / (↑x : ℂ) = 1 / (↑x : ℂ)
⊢ -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)

Tactic:
rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]

Premises used: mul_assoc, neg_neg, Complex.ofReal_one, Complex.I_mul_I, Complex.ofReal_div, neg_mul, one_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
⊢ -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)

Tactic:
have h2 : (-I * (I * ↑(1 / x))) = 1 / x := by
    rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
⊢ (↑x : ℂ) ^ (3 / 2) ≠ 0

Tactic:
simp only [Ne, cpow_eq_zero_iff, ofReal_eq_zero, hx.ne', false_and, not_false_eq_true]

Premises used: false_and, Complex.cpow_eq_zero_iff, Ne, LT.lt.ne', Complex.ofReal_eq_zero, not_false_eq_true
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
⊢ (↑x : ℂ) ^ (3 / 2) ≠ 0

Tactic:
have h3 : (x : ℂ) ^ (3 / 2 : ℂ) ≠ 0 := by
    simp only [Ne, cpow_eq_zero_iff, ofReal_eq_zero, hx.ne', false_and, not_false_eq_true]