-- 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 : ℂ)
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