-- 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
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