awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
rw :
  Tendsto
    (fun (s : ℂ) ↦
      (s - 1) *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
    (𝓝[≠] 1) (𝓝 (Φ j * (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1) * 1)))
⊢ Tendsto
    (fun (s : ℂ) ↦
      (s - 1) *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
    (𝓝[≠] 1) (𝓝 (Φ j / (↑N : ℂ)))

Tactic:
rw [(by ring : Φ j / N = Φ j * (1 / N * 1)), one_div, ← cpow_neg_one]

Premises used: Complex.cpow_neg_one, one_div
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
a b c d : ℂ
⊢ a * (b * (c * d)) = c * (b * (a * d))

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
simp :
  Tendsto
    (fun (s : ℂ) ↦
      Φ j *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * ((s - 1) * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
    (𝓝[≠] 1) (𝓝 (Φ j * (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1) * 1)))
⊢ Tendsto
    (fun (s : ℂ) ↦
      (s - 1) *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * (Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
    (𝓝[≠] 1) (𝓝 (Φ j * (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1) * 1)))

Tactic:
simp only [show ∀ a b c d : ℂ, a * (b * (c * d)) = c * (b * (a * d)) by intros; ring]
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
⊢ Tendsto
    (fun (s : ℂ) ↦
      Φ j *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * ((s - 1) * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
    (𝓝[≠] 1) (𝓝 (Φ j * (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1) * 1)))

Tactic:
tendsto_const_nhds.mul (.mul ?_ <| hurwitzZeta_residue_one _)

Premises used: tendsto_const_nhds, HurwitzZeta.hurwitzZeta_residue_one, Filter.Tendsto.mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
refine :
  Tendsto (fun (s : ℂ) ↦ HPow.hPow (α := ℂ) (↑N : ℂ) (-s)) (𝓝[≠] 1) (𝓝 (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1)))
⊢ Tendsto
    (fun (s : ℂ) ↦
      Φ j *
        (HPow.hPow (α := ℂ) (↑N : ℂ) (-s) * ((s - 1) * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s)))
    (𝓝[≠] 1) (𝓝 (Φ j * (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1) * 1)))

Tactic:
refine tendsto_const_nhds.mul (.mul ?_ <| hurwitzZeta_residue_one _)

Premises used: tendsto_const_nhds, HurwitzZeta.hurwitzZeta_residue_one, Filter.Tendsto.mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
⊢ Tendsto (fun (s : ℂ) ↦ HPow.hPow (α := ℂ) (↑N : ℂ) (-s)) (𝓝[≠] 1) (𝓝 (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1)))

Tactic:
((continuous_neg.const_cpow (Or.inl <| NeZero.ne _)).tendsto _).mono_left
    nhdsWithin_le_nhds

Premises used: ContinuousNeg.continuous_neg, Continuous.tendsto, nhdsWithin_le_nhds, Continuous.const_cpow, Filter.Tendsto.mono_left, Or.inl, NeZero.ne
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
h : Membership.mem (γ := Finset (ZMod N)) Finset.univ j
⊢ Tendsto (fun (s : ℂ) ↦ HPow.hPow (α := ℂ) (↑N : ℂ) (-s)) (𝓝[≠] 1) (𝓝 (HPow.hPow (α := ℂ) (β := ℂ) (↑N : ℂ) (-1)))

Tactic:
exact ((continuous_neg.const_cpow (Or.inl <| NeZero.ne _)).tendsto _).mono_left
    nhdsWithin_le_nhds

Premises used: ContinuousNeg.continuous_neg, Continuous.tendsto, nhdsWithin_le_nhds, Continuous.const_cpow, Filter.Tendsto.mono_left, Or.inl, NeZero.ne
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
rw :
  Eq (α := ℂ) (∑' (n : ℕ), LSeries.term (fun (x : ℕ) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * (↑x : ZMod N))) s n)
    (∑' (b : ℕ),
      cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * (↑b : ℂ)) /
        HPow.hPow (α := ℂ) (↑b : ℂ) s)
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s

Tactic:
rw [toAddCircle_apply, ← (hasSum_expZeta_of_one_lt_re (j.val / N) hs).tsum_eq,
    LFunction_eq_LSeries _ hs, LSeries]

Premises used: ZMod.LFunction_eq_LSeries, HDiv.hDiv, HurwitzZeta.hasSum_expZeta_of_one_lt_re, Nat.cast, LSeries, HasSum.tsum_eq, ZMod.toAddCircle_apply, ZMod.val
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
e_f :
  ∀ (n : ℕ),
    LSeries.term (fun (x : ℕ) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * (↑x : ZMod N))) s n =
      cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * (↑n : ℂ)) /
        HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ Eq (α := ℂ) (∑' (n : ℕ), LSeries.term (fun (x : ℕ) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * (↑x : ZMod N))) s n)
    (∑' (b : ℕ),
      cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * (↑b : ℂ)) /
        HPow.hPow (α := ℂ) (↑b : ℂ) s)

Tactic:
congr 1 with n
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
e_f :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ LSeries.term (fun (x : ℕ) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * (↑x : ZMod N))) s n =
    cexp (2 * (↑π : ℂ) * I * (↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : ℂ) * (↑n : ℂ)) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rw [LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), ofReal_div, ofReal_natCast,
    ofReal_natCast, mul_assoc, div_mul_eq_mul_div, stdAddChar_apply]

Premises used: mul_assoc, Complex.ne_zero_of_one_lt_re, div_mul_eq_mul_div, LSeries.term_of_ne_zero', Complex.ofReal_natCast, Complex.ofReal_div, ZMod.stdAddChar_apply
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ℂ) / (↑N : ℂ))

Tactic:
have := ZMod.toCircle_intCast (N := N) (j.val * n)
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ℂ) / (↑N : ℂ))
rw : cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))
| cexp (2 * (↑π : ℂ) * I * (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ℂ) / (↑N : ℂ))

Tactic:
rw [Int.cast_mul, Int.cast_natCast, Int.cast_natCast, mul_div_assoc]

Premises used: Int.cast_natCast, mul_div_assoc, Int.cast_mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ℂ) / (↑N : ℂ))
⊢ (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))

Tactic:
conv_rhs at this => rw [Int.cast_mul, Int.cast_natCast, Int.cast_natCast, mul_div_assoc]

Premises used: Int.cast_natCast, mul_div_assoc, Int.cast_mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ)))
e_f :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (↑(HMul.hMul (α := ℤ) (↑j.val : ℤ) (↑n : ℤ)) : ZMod N)) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₁ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑(↑j.val : ℤ) : ZMod N) (↑(↑n : ℤ) : ZMod N))) :
        ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₂ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑j.val : ZMod N) (↑(↑n : ℤ) : ZMod N))) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₃ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (HMul.hMul (α := ZMod N) (↑j.val : ZMod N) (↑n : ZMod N))) : ℂ) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
e_f₄ e_f₅ :
  (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (↑((toCircle : (a : ZMod N) → Circle) (j * (↑n : ZMod N))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    cexp (2 * (↑π : ℂ) * I * (HMul.hMul (α := ℂ) (↑j.val : ℂ) (↑n : ℂ) / (↑N : ℂ))) / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rw [← this, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_zmod_val]

Premises used: Int.cast_natCast, ZMod.natCast_zmod_val, Int.cast_mul
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
pos : ∀ (h : j = 0), IsOpen U
neg : ∀ (h : ¬j = 0), IsOpen U
⊢ IsOpen U

Tactic:
by_cases h : j = 0
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
h : j = 0
⊢ IsOpen U

Tactic:
simpa only [h, ↓reduceIte, U] using isOpen_compl_singleton

Premises used: isOpen_compl_singleton, reduceIte
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
h : ¬j = 0
⊢ IsOpen U

Tactic:
simp only [h, ↓reduceIte, isOpen_univ, U]

Premises used: isOpen_univ, reduceIte
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
⊢ IsOpen U

Tactic:
have hUo : IsOpen U := by
    by_cases h : j = 0
    · simpa only [h, ↓reduceIte, U] using isOpen_compl_singleton
    · simp only [h, ↓reduceIte, isOpen_univ, U]
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
u : ℂ
simp : j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
⊢ u ∈ U ↔ u ≠ 1 ∨ j ≠ 0

Tactic:
simp only [mem_ite_univ_right, U]

Premises used: Set.mem_ite_univ_right
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
⊢ ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0

Tactic:
have hU {u} : u ∈ U ↔ u ≠ 1 ∨ j ≠ 0 := by simp only [mem_ite_univ_right, U]; tauto
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
⊢ AnalyticOnNhd ℂ f U

Tactic:
DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo

Premises used: DifferentiableOn.analyticOnNhd
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
refine : ∀ (u : ℂ) (hu : u ∈ U), DifferentiableWithinAt ℂ f U u
⊢ AnalyticOnNhd ℂ f U

Tactic:
refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo

Premises used: DifferentiableOn.analyticOnNhd
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
u : ℂ
hu : u ∈ U
⊢ DifferentiableWithinAt ℂ f U u

Tactic:
(differentiableAt_LFunction _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt

Premises used: ZMod.differentiableAt_LFunction, DifferentiableAt.differentiableWithinAt, Iff.mp, Or.imp_right
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
u : ℂ
hu : u ∈ U
refine : ∀ (h : j ≠ 0), Eq (α := ℂ) (∑ j_1 : ZMod N, (𝕖 : (a : ZMod N) → ℂ) (j * j_1)) 0
⊢ DifferentiableWithinAt ℂ f U u

Tactic:
refine (differentiableAt_LFunction _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt

Premises used: ZMod.differentiableAt_LFunction, DifferentiableAt.differentiableWithinAt, Iff.mp, Or.imp_right
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
u : ℂ
hu : u ∈ U
h : j ≠ 0
⊢ Eq (α := ℂ) (∑ j_1 : ZMod N, (𝕖 : (a : ZMod N) → ℂ) (j * j_1)) 0

Tactic:
simp only [mul_comm j, AddChar.sum_mulShift _ (isPrimitive_stdAddChar _), h,
      ↓reduceIte, CharP.cast_eq_zero]

Premises used: CharP.cast_eq_zero, AddChar.sum_mulShift, ZMod.isPrimitive_stdAddChar, mul_comm, reduceIte
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
⊢ AnalyticOnNhd ℂ f U

Tactic:
have hf : AnalyticOnNhd ℂ f U := by
    refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
    refine (differentiableAt_LFunction _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
    simp only [mul_comm j, AddChar.sum_mulShift _ (isPrimitive_stdAddChar _), h,
      ↓reduceIte, CharP.cast_eq_zero]
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
⊢ AnalyticOnNhd ℂ g U

Tactic:
DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo

Premises used: DifferentiableOn.analyticOnNhd
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
refine : ∀ (u : ℂ) (hu : u ∈ U), DifferentiableWithinAt ℂ g U u
⊢ AnalyticOnNhd ℂ g U

Tactic:
refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo

Premises used: DifferentiableOn.analyticOnNhd
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
u : ℂ
hu : u ∈ U
⊢ DifferentiableWithinAt ℂ g U u

Tactic:
(differentiableAt_expZeta _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, Iff.mp, Or.imp_right, HurwitzZeta.differentiableAt_expZeta
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
u : ℂ
hu : u ∈ U
refine :
  ∀ (h : j ≠ 0),
    Ne (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle) (0 : UnitAddCircle)
⊢ DifferentiableWithinAt ℂ g U u

Tactic:
refine (differentiableAt_expZeta _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, Iff.mp, Or.imp_right, HurwitzZeta.differentiableAt_expZeta
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
u : ℂ
hu : u ∈ U
h : j ≠ 0
rwa : ¬Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle) (0 : UnitAddCircle)
rwa₁ rwa₂ rwa₃ rwa₄ : ¬j = 0
⊢ Ne (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle) (0 : UnitAddCircle)

Tactic:
rwa [ne_eq, toAddCircle_eq_zero]

Premises used: ne_eq, ZMod.toAddCircle_eq_zero
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
⊢ AnalyticOnNhd ℂ g U

Tactic:
have hg : AnalyticOnNhd ℂ g U := by
    refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
    refine (differentiableAt_expZeta _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
    rwa [ne_eq, toAddCircle_eq_zero]
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
pos : ∀ (h : j = 0), IsPreconnected U
neg : ∀ (h : ¬j = 0), IsPreconnected U
⊢ IsPreconnected U

Tactic:
by_cases h : j = 0
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
h : j = 0
⊢ 1 < Module.rank ℝ ℂ

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
h : j = 0
⊢ IsPreconnected U

Tactic:
simpa only [h, ↓reduceIte, U] using
        (isConnected_compl_singleton_of_one_lt_rank (by simp) _).isPreconnected

Premises used: isConnected_compl_singleton_of_one_lt_rank, IsConnected.isPreconnected, reduceIte
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
h : ¬j = 0
⊢ IsPreconnected U

Tactic:
simpa only [h, ↓reduceIte, U] using isPreconnected_univ

Premises used: reduceIte, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
⊢ IsPreconnected U

Tactic:
have hUc : IsPreconnected U := by
    by_cases h : j = 0
    · simpa only [h, ↓reduceIte, U] using
        (isConnected_compl_singleton_of_one_lt_rank (by simp) _).isPreconnected
    · simpa only [h, ↓reduceIte, U] using isPreconnected_univ
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z : ℂ | z ≠ 1} else Set.univ
V : Set ℂ := {z : ℂ | 1 < z.re}
hUo : IsOpen U
f : (s : ℂ) → ℂ := LFunction (N := N) fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)
g : (s : ℂ) → ℂ := expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
⊢ 2 ∈ re ⁻¹' Set.Ioi 1

Tactic:
simp