awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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 : ℂ
inl : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inr : ∀ (hjs : s ≠ 1), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inl₁ : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inr₁ : ∀ (hjs : s ≠ 1), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inl₂ : ∀ (hjs : j ≠ 0), (j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u) → u ≠ 1 ∨ j ≠ 0
inl₃ : ∀ (hjs : j ≠ 0), u ≠ 1 ∨ j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₂ : ∀ (hjs : s ≠ 1), (j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u) → u ≠ 1 ∨ j ≠ 0
inr₃ : ∀ (hjs : s ≠ 1), u ≠ 1 ∨ j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₄ : ∀ (hjs : j ≠ 0), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inl₅ : ∀ (hjs : j ≠ 0), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inl₆ : ∀ (hjs : j ≠ 0), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inl₇ : ∀ (hjs : j ≠ 0), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inl₈ : ∀ (hjs : j ≠ 0), ¬j = 0 → ¬u ≠ 1 → j ≠ 0
inl₉ : ∀ (hjs : j ≠ 0), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → ¬u ≠ 1 → j ≠ 0
inl₁₀ : ∀ (hjs : j ≠ 0), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₁ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₂ : ∀ (hjs : j ≠ 0), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₃ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₄ : ∀ (hjs : j ≠ 0), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₅ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₄ : ∀ (hjs : s ≠ 1), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inr₅ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inr₆ : ∀ (hjs : s ≠ 1), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inr₇ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inr₈ : ∀ (hjs : s ≠ 1), ¬j = 0 → ¬u ≠ 1 → j ≠ 0
inr₉ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → ¬u ≠ 1 → j ≠ 0
⊢ j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
have inr₁₀ : ∀ (hjs : s ≠ 1), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
Tactic: tauto
Cleared hypotheses: hjs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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 : ℂ
inl : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inr : ∀ (hjs : s ≠ 1), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inl₁ : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inr₁ : ∀ (hjs : s ≠ 1), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inl₂ : ∀ (hjs : j ≠ 0), (j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u) → u ≠ 1 ∨ j ≠ 0
inl₃ : ∀ (hjs : j ≠ 0), u ≠ 1 ∨ j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₂ : ∀ (hjs : s ≠ 1), (j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u) → u ≠ 1 ∨ j ≠ 0
inr₃ : ∀ (hjs : s ≠ 1), u ≠ 1 ∨ j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₄ : ∀ (hjs : j ≠ 0), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inl₅ : ∀ (hjs : j ≠ 0), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inl₆ : ∀ (hjs : j ≠ 0), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inl₇ : ∀ (hjs : j ≠ 0), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inl₈ : ∀ (hjs : j ≠ 0), ¬j = 0 → ¬u ≠ 1 → j ≠ 0
inl₉ : ∀ (hjs : j ≠ 0), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → ¬u ≠ 1 → j ≠ 0
inl₁₀ : ∀ (hjs : j ≠ 0), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₁ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₂ : ∀ (hjs : j ≠ 0), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₃ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₄ : ∀ (hjs : j ≠ 0), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₅ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₄ : ∀ (hjs : s ≠ 1), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inr₅ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inr₆ : ∀ (hjs : s ≠ 1), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inr₇ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inr₈ : ∀ (hjs : s ≠ 1), ¬j = 0 → ¬u ≠ 1 → j ≠ 0
inr₉ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → ¬u ≠ 1 → j ≠ 0
inr₁₀ : ∀ (hjs : s ≠ 1), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
⊢ j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
have inr₁₁ : ∀ (hjs : s ≠ 1), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
Tactic: tauto
Cleared hypotheses: hjs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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 : ℂ
inl : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inr : ∀ (hjs : s ≠ 1), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inl₁ : ∀ (hjs : j ≠ 0), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inr₁ : ∀ (hjs : s ≠ 1), j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
inl₂ : ∀ (hjs : j ≠ 0), (j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u) → u ≠ 1 ∨ j ≠ 0
inl₃ : ∀ (hjs : j ≠ 0), u ≠ 1 ∨ j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₂ : ∀ (hjs : s ≠ 1), (j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u) → u ≠ 1 ∨ j ≠ 0
inr₃ : ∀ (hjs : s ≠ 1), u ≠ 1 ∨ j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₄ : ∀ (hjs : j ≠ 0), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inl₅ : ∀ (hjs : j ≠ 0), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inl₆ : ∀ (hjs : j ≠ 0), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inl₇ : ∀ (hjs : j ≠ 0), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inl₈ : ∀ (hjs : j ≠ 0), ¬j = 0 → ¬u ≠ 1 → j ≠ 0
inl₉ : ∀ (hjs : j ≠ 0), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → ¬u ≠ 1 → j ≠ 0
inl₁₀ : ∀ (hjs : j ≠ 0), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₁ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₂ : ∀ (hjs : j ≠ 0), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₃ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₄ : ∀ (hjs : j ≠ 0), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inl₁₅ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₄ : ∀ (hjs : s ≠ 1), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inr₅ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inr₆ : ∀ (hjs : s ≠ 1), ¬j = 0 → u ≠ 1 ∨ j ≠ 0
inr₇ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u ≠ 1 ∨ j ≠ 0
inr₈ : ∀ (hjs : s ≠ 1), ¬j = 0 → ¬u ≠ 1 → j ≠ 0
inr₉ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → ¬u ≠ 1 → j ≠ 0
inr₁₀ : ∀ (hjs : s ≠ 1), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₁₁ : ∀ (hjs : s ≠ 1), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₁₂ : ∀ (hjs : s ≠ 1), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₁₃ : ∀ (hjs : s ≠ 1), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₁₄ : ∀ (hjs : s ≠ 1), u ≠ 1 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
inr₁₅ : ∀ (hjs : s ≠ 1), j ≠ 0 → j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u
⊢ j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
have inl₁₆ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → u = 1 → False
Tactic: tauto
Cleared hypotheses: hjs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
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)
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have hU : ∀ {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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
have refine : ∀ (u : ℂ) (hu : u ∈ U), DifferentiableWithinAt ℂ f U u
Tactic: refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
have refine : ∀ (h : j ≠ 0), Eq (α := ℂ) (∑ j_1 : ZMod N, (𝕖 : (a : ZMod N) → ℂ) (j * j_1)) 0
Tactic: refine (differentiableAt_LFunction _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
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
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have hf : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
have refine : ∀ (u : ℂ) (hu : u ∈ U), DifferentiableWithinAt ℂ g U u
Tactic: refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
have refine : ∀ (h : j ≠ 0),
  Ne (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle) (0 : UnitAddCircle)
Tactic: refine (differentiableAt_expZeta _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
⊢ Ne (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle) (0 : UnitAddCircle)
have rwa : ¬Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle) (0 : UnitAddCircle)
Tactic: rwa [ne_eq, toAddCircle_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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)
⊢ Ne (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle) (0 : UnitAddCircle)
have rwa₁ : ¬j = 0
Tactic: rwa [ne_eq, toAddCircle_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
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
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have hg : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
have pos : ∀ (h : j = 0), IsPreconnected U
Tactic: by_cases h : j = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
⊢ IsPreconnected U
have neg : ∀ (h : ¬j = 0), IsPreconnected U
Tactic: by_cases h : j = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
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
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have hUc : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
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
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
Tactic: have hV : V ∈ 𝓝 2 := (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
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
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have hUmem : 2 ∈ U
Tactic: have hUmem : 2 ∈ U := by simp [U]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (hypothesis)
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
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
hUmem : 2 ∈ U
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have hUmem' : s ∈ U
Tactic: have hUmem' : s ∈ U := hU.mpr hjs.symm
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
hUmem : 2 ∈ U
hUmem' : s ∈ U
⊢ LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (j * k)) s =
    expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s
have refine : f =ᶠ[𝓝 2] g
Tactic: refine hf.eqOn_of_preconnected_of_eventuallyEq hg hUc hUmem ?_ hUmem'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
hUmem : 2 ∈ U
hUmem' : s ∈ U
⊢ f =ᶠ[𝓝 2] g
have h : ∀ (a : ℂ),
  Membership.mem (γ := Set ℂ) {x : ℂ | x ∈ V → Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ f x = g x) x} x} a
Tactic: filter_upwards [hV] with z using LFunction_stdAddChar_eq_expZeta_of_one_lt_re _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
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
hV : Membership.mem (γ := Filter ℂ) (𝓝 2) V
hUmem : 2 ∈ U
hUmem' : s ∈ U
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ) {x : ℂ | x ∈ V → Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ f x = g x) x} x} a
⊢ f =ᶠ[𝓝 2] g
have h₁ : ∀ a ∈ V, f a = g a
Tactic: filter_upwards [hV] with z using LFunction_stdAddChar_eq_expZeta_of_one_lt_re _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have pos : ∀ (h : -j ≠ 0 ∨ s ≠ 1),
  Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
Tactic: by_cases h : -j ≠ 0 ∨ s ≠ 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
pos :
  ∀ (h : -j ≠ 0 ∨ s ≠ 1),
    Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
      Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have neg : ∀ (h : ¬(-j ≠ 0 ∨ s ≠ 1)),
  Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
Tactic: by_cases h : -j ≠ 0 ∨ s ≠ 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : -j ≠ 0 ∨ s ≠ 1
⊢ Φ j * LFunction (N := N) (fun (k : ZMod N) ↦ (𝕖 : (a : ZMod N) → ℂ) (-j * k)) s =
    Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
have pos : Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s =
  Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
Tactic: rw [LFunction_stdAddChar_eq_expZeta _ _ h]