awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
x y z : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + z) / 2) * hurwitzZetaEven a s +
      I * (2 * x * Complex.Gamma s * ((z - y) * I / 2) * hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) + z * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
have ring_nf : x * Complex.Gamma s * y * hurwitzZetaEven a s - x * Complex.Gamma s * y * HPow.hPow (β := ℕ) I 2 * hurwitzZetaOdd a s +
      x * Complex.Gamma s * z * hurwitzZetaEven a s +
    x * Complex.Gamma s * z * HPow.hPow (β := ℕ) I 2 * hurwitzZetaOdd a s =
  x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s +
      x * Complex.Gamma s * z * hurwitzZetaEven a s -
    x * Complex.Gamma s * z * hurwitzZetaOdd a s
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
x y z : ℂ
⊢ x * Complex.Gamma s * y * hurwitzZetaEven a s -
          x * Complex.Gamma s * y * HPow.hPow (β := ℕ) I 2 * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s +
      x * Complex.Gamma s * z * HPow.hPow (β := ℕ) I 2 * hurwitzZetaOdd a s =
    x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s -
      x * Complex.Gamma s * z * hurwitzZetaOdd a s
have rw : x * Complex.Gamma s * y * hurwitzZetaEven a s - x * Complex.Gamma s * y * -1 * hurwitzZetaOdd a s +
      x * Complex.Gamma s * z * hurwitzZetaEven a s +
    x * Complex.Gamma s * z * -1 * hurwitzZetaOdd a s =
  x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s +
      x * Complex.Gamma s * z * hurwitzZetaEven a s -
    x * Complex.Gamma s * z * hurwitzZetaOdd a s
Tactic: rw [I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x ξ : ℝ
⊢ Eq (α := ℝ)
    ((fun (ξ : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re)
      (ξ + 1))
    ((fun (ξ : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re)
      ξ)
have simp : rexp (-π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x) *
    (cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) *
        jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re =
  rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re
Tactic: simp only [ofReal_add, ofReal_one, add_mul, one_mul, jacobiTheta₂_add_left']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x ξ : ℝ
⊢ cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) = (↑(rexp (π * (x + 2 * ξ * x))) : ℂ)
have ring_nf : cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * (↑x : ℂ)) - (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * (↑x : ℂ) * (↑ξ : ℂ) * 2) =
  (↑(rexp (π * x + π * x * ξ * 2)) : ℂ)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
x ξ : ℝ
⊢ rexp (-π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x) *
      (cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) *
          jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re =
    rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re
have this : cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) = (↑(rexp (π * (x + 2 * ξ * x))) : ℂ)
Tactic: have : cexp (-↑π * I * ((I * ↑x) + 2 * (↑ξ * I * ↑x))) = rexp (π * (x + 2 * ξ * x)) := by
        ring_nf
        simp [I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x ξ : ℝ
this : cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) = (↑(rexp (π * (x + 2 * ξ * x))) : ℂ)
⊢ rexp (-π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x) *
      (cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) *
          jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re =
    rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re
have rw : rexp (-π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x + π * (x + 2 * ξ * x)) *
    (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re =
  rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re
Tactic: rw [this, re_ofReal_mul, ← mul_assoc, ← Real.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x ξ : ℝ
this : cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) = (↑(rexp (π * (x + 2 * ξ * x))) : ℂ)
⊢ rexp (-π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x + π * (x + 2 * ξ * x)) *
      (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re =
    rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re
have e_a : -π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x + π * (x + 2 * ξ * x) = -π * HPow.hPow (β := ℕ) ξ 2 * x
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 0
have H : ∀ (a' : ℝ), evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
Tactic: induction a using QuotientAddGroup.induction_on with
  | H a' => simp [← ofReal_inj, evenKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ cosKernel a x = 0
have H : ∀ (z : ℝ), cosKernel (↑z : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
Tactic: induction a using QuotientAddGroup.induction_on with
  | H => simp [← ofReal_inj, cosKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
⊢ evenKernel 0 = cosKernel 0
have h : ∀ (x : ℝ), evenKernel 0 x = cosKernel 0 x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x : ℝ
⊢ evenKernel (-a) x = evenKernel a x
have H : ∀ (z : ℝ), evenKernel (-(↑z : ℝ ⧸ AddSubgroup.zmultiples 1)) x = evenKernel (↑z : ℝ ⧸ AddSubgroup.zmultiples 1) x
Tactic: induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, evenKernel_def, jacobiTheta₂_neg_left]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x : ℝ
⊢ cosKernel (-a) x = cosKernel a x
have H : ∀ (z : ℝ), cosKernel (-(↑z : ℝ ⧸ AddSubgroup.zmultiples 1)) x = cosKernel (↑z : ℝ ⧸ AddSubgroup.zmultiples 1) x
Tactic: induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, cosKernel_def]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a' : ℝ
⊢ ContinuousOn (evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
have H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
Tactic: apply continuous_re.comp_continuousOn (f := fun x ↦ (evenKernel a' x : ℂ))
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a' : ℝ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
have H : ContinuousOn (Y := ℂ)
  (fun (x : ℝ) ↦
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a' : ℂ) 2 * (↑x : ℂ)) *
      jacobiTheta₂ ((↑a' : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
  (Ioi 0)
Tactic: simp only [evenKernel_def]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a' : ℝ
⊢ ContinuousOn (Y := ℂ)
    (fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a' : ℂ) 2 * (↑x : ℂ)) *
        jacobiTheta₂ ((↑a' : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (Ioi 0)
have H : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ ((↑a' : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) x
Tactic: refine continuousOn_of_forall_continuousAt (fun x hx ↦ .mul (by fun_prop) ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ ContinuousOn (evenKernel a) (Ioi 0)
have H : ∀ (a' : ℝ), ContinuousOn (evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
Tactic: induction a using QuotientAddGroup.induction_on with | H a' =>
  apply continuous_re.comp_continuousOn (f := fun x ↦ (evenKernel a' x : ℂ))
  simp only [evenKernel_def]
  refine continuousOn_of_forall_continuousAt (fun x hx ↦ .mul (by fun_prop) ?_)
  exact (continuousAt_jacobiTheta₂ (a' * I * x) <| by simpa).comp
    (f := fun u : ℝ ↦ (a' * I * u, I * u)) (by fun_prop)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a' : ℝ
⊢ ContinuousOn (cosKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
have H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(cosKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
Tactic: apply continuous_re.comp_continuousOn (f := fun x ↦ (cosKernel a' x : ℂ))
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a' : ℝ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(cosKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
have H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ (↑a' : ℂ) (I * (↑x : ℂ))) (Ioi 0)
Tactic: simp only [cosKernel_def]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a' : ℝ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ (↑a' : ℂ) (I * (↑x : ℂ))) (Ioi 0)
have H : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ (↑a' : ℂ) (I * (↑x : ℂ))) x
Tactic: refine continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ ContinuousOn (cosKernel a) (Ioi 0)
have H : ∀ (a' : ℝ), ContinuousOn (cosKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
Tactic: induction a using QuotientAddGroup.induction_on with | H a' =>
  apply continuous_re.comp_continuousOn (f := fun x ↦ (cosKernel a' x : ℂ))
  simp only [cosKernel_def]
  refine continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)
  exact (continuousAt_jacobiTheta₂ a' <| by simpa).comp
    (f := fun u : ℝ ↦ ((a' : ℂ), I * u)) (by fun_prop)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x : ℝ
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
have inl : ∀ (hx : x ≤ 0), evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x : ℝ
inl : ∀ (hx : x ≤ 0), evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
have inr : ∀ (hx : 0 < x), evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
have inl : 1 / x ≤ 0
Tactic: rw [evenKernel_undef _ hx, cosKernel_undef, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
⊢ evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (1 / 2) * cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)
have inr : cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
        cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
      jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
  (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
Tactic: rw [← ofReal_inj, ofReal_mul, evenKernel_def, cosKernel_def, jacobiTheta₂_functional_equation]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
⊢ I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
have push_cast : I * (1 / (↑x : ℂ)) = -1 / (I * (↑x : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
⊢ I * (1 / (↑x : ℂ)) = -1 / (I * (↑x : ℂ))
have rw : I * (1 / (↑x : ℂ)) = -1 / I / (↑x : ℂ)
Tactic: rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
rw : I * (1 / (↑x : ℂ)) = -1 / I / (↑x : ℂ)
⊢ I * (1 / (↑x : ℂ)) = -1 / (I * (↑x : ℂ))
have rw₁ : I / (↑x : ℂ) = -1 / I / (↑x : ℂ)
Tactic: rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
rw : I * (1 / (↑x : ℂ)) = -1 / I / (↑x : ℂ)
rw₁ : I / (↑x : ℂ) = -1 / I / (↑x : ℂ)
⊢ I * (1 / (↑x : ℂ)) = -1 / (I * (↑x : ℂ))
have rw₂ : I / (↑x : ℂ) = -(-1 * I) / (↑x : ℂ)
Tactic: rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
rw : I * (1 / (↑x : ℂ)) = -1 / I / (↑x : ℂ)
rw₁ : I / (↑x : ℂ) = -1 / I / (↑x : ℂ)
rw₂ : I / (↑x : ℂ) = -(-1 * I) / (↑x : ℂ)
⊢ I * (1 / (↑x : ℂ)) = -1 / (I * (↑x : ℂ))
have rw₃ : I / (↑x : ℂ) = - -I / (↑x : ℂ)
Tactic: rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
rw : I * (1 / (↑x : ℂ)) = -1 / I / (↑x : ℂ)
rw₁ : I / (↑x : ℂ) = -1 / I / (↑x : ℂ)
rw₂ : I / (↑x : ℂ) = -(-1 * I) / (↑x : ℂ)
rw₃ : I / (↑x : ℂ) = - -I / (↑x : ℂ)
⊢ I * (1 / (↑x : ℂ)) = -1 / (I * (↑x : ℂ))
have rw₄ : I / (↑x : ℂ) = I / (↑x : ℂ)
Tactic: rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
Tactic: have h1 : I * ↑(1 / x) = -1 / (I * x) := by
    push_cast
    rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have hx' : I * (↑x : ℂ) ≠ 0
Tactic: have hx' : I * x ≠ 0 := mul_ne_zero I_ne_zero (ofReal_ne_zero.mpr hx.ne')
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
⊢ (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
have rw : (↑a : ℂ) * I * (↑x : ℂ) = (↑a : ℂ) * (I * (↑x : ℂ))
Tactic: rw [div_eq_iff hx']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
Tactic: have h2 : a * I * x / (I * x) = a := by
    rw [div_eq_iff hx']
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
⊢ 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
have rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
Tactic: rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
⊢ 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
have rw₁ : 1 / (-(I * I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
Tactic: rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₁ : 1 / (-(I * I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
⊢ 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
have rw₂ : 1 / (-(-1 * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
Tactic: rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₁ : 1 / (-(I * I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₂ : 1 / (-(-1 * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
⊢ 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
have rw₃ : 1 / (- -(↑x : ℂ)) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
Tactic: rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₁ : 1 / (-(I * I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₂ : 1 / (-(-1 * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₃ : 1 / (- -(↑x : ℂ)) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
⊢ 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
have rw₄ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
Tactic: rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₁ : 1 / (-(I * I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₂ : 1 / (-(-1 * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₃ : 1 / (- -(↑x : ℂ)) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₄ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
⊢ 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
have rw₅ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ (↑(1 / 2) : ℂ)
Tactic: rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₁ : 1 / (-(I * I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₂ : 1 / (-(-1 * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₃ : 1 / (- -(↑x : ℂ)) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₄ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₅ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ (↑(1 / 2) : ℂ)
⊢ 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
have rw₆ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
Tactic: rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₁ : 1 / (-(I * I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₂ : 1 / (-(-1 * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₃ : 1 / (- -(↑x : ℂ)) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₄ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₅ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ (↑(1 / 2) : ℂ)
rw₆ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
⊢ 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
have rw₇ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ (1 / (↑2 : ℂ))
Tactic: rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₁ : 1 / (-(I * I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₂ : 1 / (-(-1 * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₃ : 1 / (- -(↑x : ℂ)) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₄ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₅ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ (↑(1 / 2) : ℂ)
rw₆ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
rw₇ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ (1 / (↑2 : ℂ))
⊢ 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
have rw₈ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 1 2
Tactic: rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
Tactic: have h3 : 1 / (-I * (I * x)) ^ (1 / 2 : ℂ) = 1 / ↑(x ^ (1 / 2 : ℝ)) := by
    rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]