awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hχ : χ ≠ 1), Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
⊢ s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hχ : χ ≠ 1), Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
⊢ s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have inr₃ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
  s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hχ : χ ≠ 1), Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₆ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₄ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₆ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
⊢ s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have inl₇ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hχ : χ ≠ 1), Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₆ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₄ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₆ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₇ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
⊢ s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have inl₈ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
  ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hχ : χ ≠ 1), Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₆ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₄ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₆ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₇ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₈ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
⊢ s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have inl₉ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
  ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hχ : χ ≠ 1), Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₆ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₄ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₆ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₇ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₈ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₉ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
⊢ s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have inr₇ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : ∀ (hχ : χ ≠ 1), Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₆ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₄ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₆ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₇ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₈ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inl₉ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
    ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
inr₇ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬χ ≠ 1), ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
⊢ s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have inr₈ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0),
  ¬s ≠ 1 → Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
⊢ Differentiable ℂ (completedLFunction χ)
have refine : ∀ (s : ℂ), N ≠ 1
Tactic: refine fun s ↦ differentiableAt_completedLFunction _ _ (Or.inr ?_) (Or.inr hχ)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s
have inl : ∀ (hχ : χ.Even), LFunction χ s = completedLFunction χ s / χ.gammaFactor s
Tactic: rcases χ.even_or_odd with hχ | hχ
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
inl : ∀ (hχ : χ.Even), LFunction χ s = completedLFunction χ s / χ.gammaFactor s
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s
have inr : ∀ (hχ : χ.Odd), LFunction χ s = completedLFunction χ s / χ.gammaFactor s
Tactic: rcases χ.even_or_odd with hχ | hχ
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Even
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s
have inl : LFunction χ s = completedLFunction χ s / s.Gammaℝ
Tactic: rw [hχ.gammaFactor_def]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Odd
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s
have inr : LFunction χ s = completedLFunction χ s / (s + 1).Gammaℝ
Tactic: rw [hχ.gammaFactor_def]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
⊢ completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
have inl : ∀ [inst : NeZero (R := ℕ) 1] {χ : DirichletCharacter ℂ 1} (hχ : χ.IsPrimitive),
  completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑1 : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
Tactic: rcases eq_or_ne N 1 with rfl | hN
Cleared hypotheses: N, inst, χ, hχ
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
inl :
  ∀ [inst : NeZero (R := ℕ) 1] {χ : DirichletCharacter ℂ 1} (hχ : χ.IsPrimitive),
    completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑1 : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
⊢ completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
have inr : ∀ (hN : N ≠ 1),
  completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
Tactic: rcases eq_or_ne N 1 with rfl | hN
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
⊢ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have refine : ∀ (h : χ = 1), 1 = N
Tactic: refine χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h : χ = 1
⊢ 1 = N
have rwa : ∀ (hχ : χ.conductor = N) (s : ℂ) (hN : N ≠ 1) (h : χ = 1), 1 = N
Tactic: rwa [IsPrimitive, h, conductor_one] at hχ
Cleared hypotheses: hχ, s, hN, h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h : χ = 1
rwa : ∀ (hχ : χ.conductor = N) (s : ℂ) (hN : N ≠ 1) (h : χ = 1), 1 = N
⊢ 1 = N
have rwa₁ : ∀ (hχ : conductor (R := ℂ) (n := N) 1 = N) (s : ℂ) (hN : N ≠ 1) (h : χ = 1), 1 = N
Tactic: rwa [IsPrimitive, h, conductor_one] at hχ
Cleared hypotheses: hχ, s, hN, h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h : χ = 1
rwa : ∀ (hχ : χ.conductor = N) (s : ℂ) (hN : N ≠ 1) (h : χ = 1), 1 = N
rwa₁ : ∀ (hχ : conductor (R := ℂ) (n := N) 1 = N) (s : ℂ) (hN : N ≠ 1) (h : χ = 1), 1 = N
⊢ 1 = N
have rwa₂ : ∀ (hχ : 1 = N) (s : ℂ) (hN : N ≠ 1) (h : χ = 1), 1 = N
Tactic: rwa [IsPrimitive, h, conductor_one] at hχ
Cleared hypotheses: hχ, s, hN, h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
⊢ completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
have h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
Tactic: have h_sum : ∑ j, χ j = 0 := by
    refine χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)
    rwa [IsPrimitive, h, conductor_one] at hχ
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
⊢ completedLFunction χ (1 - s) = HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s
have inr : completedLFunction χ (1 - s) =
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) * gaussSum χ stdAddChar *
    completedLFunction χ⁻¹ s
Tactic: rw [rootNumber, ← mul_comm_div, ← mul_comm_div, ← cpow_sub _ _ (NeZero.ne _), sub_sub, add_halves]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
⊢ completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
have pos : ∀ (h : χ.Even),
  completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I 0 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
Tactic: split_ifs with h