awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
H :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑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)
have 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
Tactic: refine fun x hx ↦ ((Continuous.continuousAt ?_).mul ?_).continuousWithinAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a 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
have hf : Continuous (Y := ℂ × ℂ) fun (u : ℝ) ↦ ((↑a : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))
Tactic: have hf : Continuous fun u : ℝ ↦ (a * I * u, I * u) := by fun_prop
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    x
have H : ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I)) x
Tactic: apply ContinuousAt.add
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ ContinuousAt (Y := ℂ)
    (fun (x : ℝ) ↦
      jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    x
have H₁ : ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) x
Tactic: apply ContinuousAt.add
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hf : Continuous (Y := ℂ × ℂ) fun (u : ℝ) ↦ ((↑a : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))
⊢ 0 < (I * (↑x : ℂ)).im
have rwa : 0 < (↑x : ℂ).re
Tactic: rwa [I_mul_im, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hf : Continuous (Y := ℂ × ℂ) fun (u : ℝ) ↦ ((↑a : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))
rwa : 0 < (↑x : ℂ).re
⊢ 0 < (I * (↑x : ℂ)).im
have rwa₁ : 0 < x
Tactic: rwa [I_mul_im, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
⊢ ContinuousOn (oddKernel a) (Ioi 0)
have H : ∀ (a : ℝ), ContinuousOn (oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) (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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
⊢ ContinuousOn (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
have H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
Tactic: suffices ContinuousOn (fun x ↦ (sinKernel a x : ℂ)) (Ioi 0) from
    (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
have H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ))) (Ioi 0)
Tactic: simp_rw [sinKernel_def]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ))) (Ioi 0)
have apply : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ))) x
Tactic: apply (continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)).div_const
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < (I * (↑x : ℂ)).im
have rwa : 0 < (↑x : ℂ).re
Tactic: rwa [I_mul_im, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rwa : 0 < (↑x : ℂ).re
⊢ 0 < (I * (↑x : ℂ)).im
have rwa₁ : ℂ
Tactic: rwa [I_mul_im, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rwa : 0 < (↑x : ℂ).re
rwa₁ : ℂ
⊢ 0 < (I * (↑x : ℂ)).im
have rwa₂ : 0 < x
Tactic: rwa [I_mul_im, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ))) x
have h : 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])
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
⊢ ContinuousOn (sinKernel a) (Ioi 0)
have H : ∀ (a : ℝ), ContinuousOn (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) (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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
have inl : ∀ (hx : x ≤ 0), oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
inl : ∀ (hx : x ≤ 0), oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
have inr : ∀ (hx : 0 < x), oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
have inl : 0 = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
Tactic: rw [oddKernel_undef _ hx, sinKernel_undef _ (one_div_nonpos.mpr hx), mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
inl : 0 = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
have inl₁ : 0 = 1 / x ^ (3 / 2) * 0
Tactic: rw [oddKernel_undef _ hx, sinKernel_undef _ (one_div_nonpos.mpr hx), mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
inl : 0 = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
inl₁ : 0 = 1 / x ^ (3 / 2) * 0
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
have inl₂ : Eq (α := ℝ) 0 0
Tactic: rw [oddKernel_undef _ hx, sinKernel_undef _ (one_div_nonpos.mpr hx), mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw : -1 / (I * (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
rw : -1 / (I * (↑x⁻¹ : ℂ)) = I * (↑x : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₁ : -1 / (I * (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
rw : -1 / (I * (↑x⁻¹ : ℂ)) = I * (↑x : ℂ)
rw₁ : -1 / (I * (↑x : ℂ)⁻¹) = I * (↑x : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₂ : -1 / ((↑x : ℂ)⁻¹ * I) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
rw : -1 / (I * (↑x⁻¹ : ℂ)) = I * (↑x : ℂ)
rw₁ : -1 / (I * (↑x : ℂ)⁻¹) = I * (↑x : ℂ)
rw₂ : -1 / ((↑x : ℂ)⁻¹ * I) = I * (↑x : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₃ : -1 / (↑x : ℂ)⁻¹ / I = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₄ : -1 * (↑x : ℂ) / I = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₅ : -1 * (↑x : ℂ) * I⁻¹ = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₆ : -1 * (↑x : ℂ) * -I = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₇ : -(-1 * (↑x : ℂ) * I) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₈ : -(-(↑x : ℂ) * I) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₉ : - -((↑x : ℂ) * I) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₁₀ : (↑x : ℂ) * I = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
have rw₁₁ : I * (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
⊢ oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (3 / 2) * sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)
have h1 : -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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
⊢ -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
have rw : -I * I * (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
Tactic: rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
rw : -I * I * (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
⊢ -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
have rw₁ : -(I * I) * (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
Tactic: rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
have rw₂ : - -1 * (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
Tactic: rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
have rw₃ : 1 * (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
Tactic: rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
have rw₄ : (↑(1 / x) : ℂ) = 1 / (↑x : ℂ)
Tactic: rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
have rw₅ : (↑1 : ℂ) / (↑x : ℂ) = 1 / (↑x : ℂ)
Tactic: rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ)
⊢ -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
have rw₆ : 1 / (↑x : ℂ) = 1 / (↑x : ℂ)
Tactic: rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
⊢ oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (3 / 2) * sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)
have h2 : -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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
⊢ oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (3 / 2) * sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)
have h3 : (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
⊢ (↑x : ℂ).arg ≠ π
have rw : 0 ≠ π
Tactic: rw [arg_ofReal_of_nonneg hx.le]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
⊢ oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (3 / 2) * sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)
have h4 : (↑x : ℂ).arg ≠ π
Tactic: have h4 : arg x ≠ π := by rw [arg_ofReal_of_nonneg hx.le]; exact pi_ne_zero.symm
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
⊢ oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (3 / 2) * sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)
have inr : jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
  (↑(1 / x ^ (3 / 2)) : ℂ) *
    (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ)))
Tactic: rw [← ofReal_inj, oddKernel_def, ofReal_mul, sinKernel_def, jacobiTheta₂'_functional_equation',
    h1, h2]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
⊢ jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
    (↑(1 / x ^ (3 / 2)) : ℂ) *
      (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ)))
have inr : ∀ (J : ℂ), J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
Tactic: generalize jacobiTheta₂'' a (I * ↑x) = J
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]