-- 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
inl₁₆ : ∀ (hjs : j ≠ 0), j ≠ 0 → j = 0 → u = 1 → False
⊢ j = 0 → Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u ↔ u ≠ 1 ∨ j ≠ 0
have inr₁₆ : ∀ (hjs : s ≠ 1), Membership.mem (γ := Set ℂ) {z : ℂ | z ≠ 1} u → u = 1 → j = 0 → False
Tactic: tauto
Cleared hypotheses: hjs