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 : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (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 : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inr₁ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
  s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (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 : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (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 : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inr₃ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
  s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (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 : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₆ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₇ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₄ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inl₈ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (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 : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₆ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₇ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₄ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₈ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inl₉ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
  ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (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 : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₆ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₇ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₄ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₈ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₉ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inl₁₀ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (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 : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₆ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₇ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₄ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₈ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₉ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁₀ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inl₁₁ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
  ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (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 : ∀ (hn : N ≠ 1), Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₂ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₃ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₁ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₂ : ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₃ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₄ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₅ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₆ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₇ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₄ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inr₅ :
  ∀ (hs₀ : N ≠ 1) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₈ : ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : ¬N ≠ 1), ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₉ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁₀ : ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : ¬N ≠ 1), ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
inl₁₁ :
  ∀ (hs₀ : s ≠ 0) (hs₁ : χ ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
    ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ s ≠ 0 ∨ Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
have inr₆ : ∀ (hs₀ : N ≠ 1) (hs₁ : s ≠ 1) (this : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)),
  ¬s ≠ 0 → Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) 0 : ℂ) (0 : ℂ)
Tactic: tauto
Cleared hypotheses: hs₀, hs₁, this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have this : ∀ (hχ : χ ≠ 1), Eq (α := ℂ) (∑ a : ZMod N, (χ : (a : ZMod N) → ℂ) a) 0
Tactic: have := χ.sum_eq_zero_of_ne_one
-- 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
⊢ 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
⊢ 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
⊢ s ≠ 1 ∨ Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
have inl₂ : ∀ (hs₀ : s ≠ 0) (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
⊢ 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
⊢ 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
⊢ 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