awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ B.F s = LSeries (⇑B.χ.zetaMul : (a : ℕ) → ℂ) s
have rw : Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
  LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
    LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
Tactic: rw [F, zetaMul, ← coe_mul, LSeries_convolution']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
rw :
  Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
⊢ B.F s = LSeries (⇑B.χ.zetaMul : (a : ℕ) → ℂ) s
have hf : LSeriesSummable (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s
Tactic: rw [F, zetaMul, ← coe_mul, LSeries_convolution']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
rw :
  Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
hf : LSeriesSummable (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s
⊢ B.F s = LSeries (⇑B.χ.zetaMul : (a : ℕ) → ℂ) s
have hg : LSeriesSummable (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
Tactic: rw [F, zetaMul, ← coe_mul, LSeries_convolution']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
have hs' : s ≠ 1
Tactic: have hs' : s ≠ 1 := fun h ↦ by simp only [h, one_re, lt_self_iff_false] at hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
have simp : riemannZeta s * LSeries (fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s =
  LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
    LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
Tactic: simp only [ne_eq, hs', not_false_eq_true, Function.update_of_ne, B.χ.LFunction_eq_LSeries hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ riemannZeta s * LSeries (fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
have e_a : riemannZeta s = LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
e_a : riemannZeta s = LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s
⊢ riemannZeta s * LSeries (fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
have e_a₁ : LSeries (fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s =
  LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ riemannZeta s = LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s
have e_a : LSeries (fun (n : ℕ) ↦ (↑((zeta : (a : ℕ) → ℕ) n) : ℂ)) s = LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s
Tactic: simp_rw [← LSeries_zeta_eq_riemannZeta hs, ← natCoe_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
⊢ DifferentiableAt ℂ B.F s
have inl : ∀ (hs : s ≠ 1), DifferentiableAt ℂ B.F s
Tactic: rcases ne_or_eq s 1 with hs | rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
inl : ∀ (hs : s ≠ 1), DifferentiableAt ℂ B.F s
⊢ DifferentiableAt ℂ B.F s
have inr : DifferentiableAt ℂ B.F 1
Tactic: rcases ne_or_eq s 1 with hs | rfl
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
⊢ DifferentiableAt ℂ B.F 1
have inr : ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ B.F z
Tactic: refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt ?_ ?_).differentiableAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
inr : ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ B.F z
⊢ DifferentiableAt ℂ B.F 1
have inr₁ : ContinuousAt B.F 1
Tactic: refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt ?_ ?_).differentiableAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ B.F z
have h : ∀ (t : ℂ) (ht : Membership.mem (γ := Set ℂ) {1}ᶜ t), DifferentiableAt ℂ B.F t
Tactic: filter_upwards [self_mem_nhdsWithin] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
⊢ B.F = G * H
have h : ∀ (t : ℂ), B.F t = (G * H) t
Tactic: ext1 t
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
t : ℂ
⊢ B.F t = (G * H) t
have h : B.F 1 = (G * H) 1
Tactic: rcases eq_or_ne t 1 with rfl | ht
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
t : ℂ
h : B.F 1 = (G * H) 1
⊢ B.F t = (G * H) t
have h₁ : ∀ (ht : t ≠ 1), B.F t = (G * H) t
Tactic: rcases eq_or_ne t 1 with rfl | ht
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
⊢ ContinuousAt B.F 1
have this : B.F = G * H
Tactic: have : B.F = G * H := by
    ext1 t
    rcases eq_or_ne t 1 with rfl | ht
    · simp only [F, G, H, Pi.mul_apply, one_mul, Function.update_self]
    · simp only [F, G, H, Function.update_of_ne ht, mul_comm _ (riemannZeta _), B.hχ, sub_zero,
      Pi.mul_apply, mul_assoc, mul_div_cancel₀ _ (sub_ne_zero.mpr ht)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt B.F 1
have inr : ContinuousAt (G * H) 1
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt (G * H) 1
have inr : ContinuousAt G 1
Tactic: apply ContinuousAt.mul
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
G : (a : ℂ) → ℂ := Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) 1 1
H : (a : ℂ) → ℂ :=
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1
    (deriv (LFunction B.χ) 1)
this : B.F = G * H
inr : ContinuousAt G 1
⊢ ContinuousAt (G * H) 1
have inr₁ : ContinuousAt H 1
Tactic: apply ContinuousAt.mul
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
⊢ B.F (↑(-2) : ℂ) = 0
have this : riemannZeta (-2 * HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) = 0
Tactic: have := riemannZeta_neg_two_mul_nat_add_one 0
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2 * HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1) = 0
⊢ B.F (↑(-2) : ℂ) = 0
have this₁ : riemannZeta (-2) = 0
Tactic: rw [Nat.cast_zero, zero_add, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ B.F (↑(-2) : ℂ) = 0
have rw : Eq (α := ℂ)
  (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
      (↑(-2) : ℂ) :
    ℂ)
  (0 : ℂ)
Tactic: rw [F, ofReal_neg, ofReal_ofNat, Function.update_of_ne (mod_cast (by lia : (-2 : ℤ) ≠ 1)),
    this, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (↑(-2) : ℂ) :
      ℂ)
    (0 : ℂ)
⊢ B.F (↑(-2) : ℂ) = 0
have rw₁ : Eq (α := ℂ)
  (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
      (-(↑2 : ℂ)) :
    ℂ)
  (0 : ℂ)
Tactic: rw [F, ofReal_neg, ofReal_ofNat, Function.update_of_ne (mod_cast (by lia : (-2 : ℤ) ≠ 1)),
    this, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (↑(-2) : ℂ) :
      ℂ)
    (0 : ℂ)
rw₁ :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (-(↑2 : ℂ)) :
      ℂ)
    (0 : ℂ)
⊢ B.F (↑(-2) : ℂ) = 0
have rw₂ : Eq (α := ℂ)
  (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
      (-2) :
    ℂ)
  (0 : ℂ)
Tactic: rw [F, ofReal_neg, ofReal_ofNat, Function.update_of_ne (mod_cast (by lia : (-2 : ℤ) ≠ 1)),
    this, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (↑(-2) : ℂ) :
      ℂ)
    (0 : ℂ)
rw₁ :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (-(↑2 : ℂ)) :
      ℂ)
    (0 : ℂ)
rw₂ :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (-2) :
      ℂ)
    (0 : ℂ)
⊢ B.F (↑(-2) : ℂ) = 0
have rw₃ : riemannZeta (-2) * LFunction B.χ (-2) = 0
Tactic: rw [F, ofReal_neg, ofReal_ofNat, Function.update_of_ne (mod_cast (by lia : (-2 : ℤ) ≠ 1)),
    this, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (↑(-2) : ℂ) :
      ℂ)
    (0 : ℂ)
rw₁ :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (-(↑2 : ℂ)) :
      ℂ)
    (0 : ℂ)
rw₂ :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (-2) :
      ℂ)
    (0 : ℂ)
rw₃ : riemannZeta (-2) * LFunction B.χ (-2) = 0
⊢ B.F (↑(-2) : ℂ) = 0
have rw₄ : 0 * LFunction B.χ (-2) = 0
Tactic: rw [F, ofReal_neg, ofReal_ofNat, Function.update_of_ne (mod_cast (by lia : (-2 : ℤ) ≠ 1)),
    this, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (↑(-2) : ℂ) :
      ℂ)
    (0 : ℂ)
rw₁ :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (-(↑2 : ℂ)) :
      ℂ)
    (0 : ℂ)
rw₂ :
  Eq (α := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1)
        (-2) :
      ℂ)
    (0 : ℂ)
rw₃ : riemannZeta (-2) * LFunction B.χ (-2) = 0
rw₄ : 0 * LFunction B.χ (-2) = 0
⊢ B.F (↑(-2) : ℂ) = 0
have rw₅ : Eq (α := ℂ) 0 0
Tactic: rw [F, ofReal_neg, ofReal_ofNat, Function.update_of_ne (mod_cast (by lia : (-2 : ℤ) ≠ 1)),
    this, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ False
have refine : 0 < B.F (↑(-2) : ℂ)
Tactic: refine B.F_neg_two.not_gt ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ 0 < B.F (↑(-2) : ℂ)
have refine : LSeries.abscissaOfAbsConv (⇑χ.zetaMul : (a : ℕ) → ℂ) ≤ (↑1 : EReal)
Tactic: refine ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn (zetaMul_nonneg hχ)
    (χ.isMultiplicative_zetaMul.map_one ▸ zero_lt_one) B.F_differentiable ?_
    (fun _ ↦ B.F_eq_LSeries) _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
⊢ 0 ≤
    3 * (-log (1 - (↑a : ℂ))).re + 4 * (-log (1 - (↑a : ℂ) * z)).re + (-log (1 - (↑a : ℂ) * HPow.hPow (β := ℕ) z 2)).re
have hac₀ : ‖(↑a : ℂ)‖ < 1
Tactic: have hac₀ : ‖(a : ℂ)‖ < 1 := by
    simp only [Complex.norm_of_nonneg ha₀, ha₁]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
⊢ ‖(↑a : ℂ) * z‖ < 1
have rwa : ‖(↑a : ℂ)‖ * ‖z‖ < 1
Tactic: rwa [norm_mul, hz, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
rwa : ‖(↑a : ℂ)‖ * ‖z‖ < 1
⊢ ‖(↑a : ℂ) * z‖ < 1
have rwa₁ : ‖(↑a : ℂ)‖ * 1 < 1
Tactic: rwa [norm_mul, hz, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
⊢ 0 ≤
    3 * (-log (1 - (↑a : ℂ))).re + 4 * (-log (1 - (↑a : ℂ) * z)).re + (-log (1 - (↑a : ℂ) * HPow.hPow (β := ℕ) z 2)).re
have hac₁ : ‖(↑a : ℂ) * z‖ < 1
Tactic: have hac₁ : ‖a * z‖ < 1 := by rwa [norm_mul, hz, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
⊢ ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
have rwa : ‖(↑a : ℂ)‖ * ‖HPow.hPow (β := ℕ) z 2‖ < 1
Tactic: rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
rwa : ‖(↑a : ℂ)‖ * ‖HPow.hPow (β := ℕ) z 2‖ < 1
⊢ ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
have rwa₁ : ‖(↑a : ℂ)‖ * HPow.hPow (β := ℕ) ‖z‖ 2 < 1
Tactic: rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
rwa : ‖(↑a : ℂ)‖ * ‖HPow.hPow (β := ℕ) z 2‖ < 1
rwa₁ : ‖(↑a : ℂ)‖ * HPow.hPow (β := ℕ) ‖z‖ 2 < 1
⊢ ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
have rwa₂ : ‖(↑a : ℂ)‖ * HPow.hPow (α := ℝ) (β := ℕ) 1 2 < 1
Tactic: rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
rwa : ‖(↑a : ℂ)‖ * ‖HPow.hPow (β := ℕ) z 2‖ < 1
rwa₁ : ‖(↑a : ℂ)‖ * HPow.hPow (β := ℕ) ‖z‖ 2 < 1
rwa₂ : ‖(↑a : ℂ)‖ * HPow.hPow (α := ℝ) (β := ℕ) 1 2 < 1
⊢ ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
have rwa₃ : ‖(↑a : ℂ)‖ * 1 < 1
Tactic: rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
⊢ 0 ≤
    3 * (-log (1 - (↑a : ℂ))).re + 4 * (-log (1 - (↑a : ℂ) * z)).re + (-log (1 - (↑a : ℂ) * HPow.hPow (β := ℕ) z 2)).re
have hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
Tactic: have hac₂ : ‖a * z ^ 2‖ < 1 := by rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
⊢ 0 ≤
    3 * (-log (1 - (↑a : ℂ))).re + 4 * (-log (1 - (↑a : ℂ) * z)).re + (-log (1 - (↑a : ℂ) * HPow.hPow (β := ℕ) z 2)).re
have rw : LE.le (α := ℝ) 0
  (∑' (b : ℕ),
    (3 * ((↑a : ℂ) ^ b / (↑b : ℂ)).re + 4 * (((↑a : ℂ) * z) ^ b / (↑b : ℂ)).re +
      (((↑a : ℂ) * HPow.hPow (β := ℕ) z 2) ^ b / (↑b : ℂ)).re))
Tactic: rw [← ((hasSum_re <| hasSum_taylorSeries_neg_log hac₀).mul_left 3).add
    ((hasSum_re <| hasSum_taylorSeries_neg_log hac₁).mul_left 4) |>.add
    (hasSum_re <| hasSum_taylorSeries_neg_log hac₂) |>.tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
⊢ LE.le (α := ℝ) 0
    (∑' (b : ℕ),
      (3 * ((↑a : ℂ) ^ b / (↑b : ℂ)).re + 4 * (((↑a : ℂ) * z) ^ b / (↑b : ℂ)).re +
        (((↑a : ℂ) * HPow.hPow (β := ℕ) z 2) ^ b / (↑b : ℂ)).re))
have refine : ∀ (n : ℕ),
  0 ≤
    3 * ((↑a : ℂ) ^ n / (↑n : ℂ)).re + 4 * (((↑a : ℂ) * z) ^ n / (↑n : ℂ)).re +
      (((↑a : ℂ) * HPow.hPow (β := ℕ) z 2) ^ n / (↑n : ℂ)).re
Tactic: refine tsum_nonneg fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
⊢ 0 ≤
    3 * ((↑a : ℂ) ^ n / (↑n : ℂ)).re + 4 * (((↑a : ℂ) * z) ^ n / (↑n : ℂ)).re +
      (((↑a : ℂ) * HPow.hPow (β := ℕ) z 2) ^ n / (↑n : ℂ)).re
have simp : 0 ≤ 3 * (a ^ n / (↑n : ℝ)) + 4 * (a ^ n * (z ^ n).re / (↑n : ℝ)) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re / (↑n : ℝ)
Tactic: simp only [← ofReal_pow, div_natCast_re, ofReal_re, mul_pow, mul_re, ofReal_im, zero_mul,
    sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (a ^ n / (↑n : ℝ)) + 4 * (a ^ n * (z ^ n).re / (↑n : ℝ)) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re / (↑n : ℝ)
have inl : 0 ≤
  3 * (HPow.hPow (β := ℕ) a 0 / (↑0 : ℝ)) + 4 * (HPow.hPow (β := ℕ) a 0 * (HPow.hPow (β := ℕ) z 0).re / (↑0 : ℝ)) +
    HPow.hPow (β := ℕ) a 0 * (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) z 2) 0).re / (↑0 : ℝ)
Tactic: rcases n.eq_zero_or_pos with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
inl :
  0 ≤
    3 * (HPow.hPow (β := ℕ) a 0 / (↑0 : ℝ)) + 4 * (HPow.hPow (β := ℕ) a 0 * (HPow.hPow (β := ℕ) z 0).re / (↑0 : ℝ)) +
      HPow.hPow (β := ℕ) a 0 * (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) z 2) 0).re / (↑0 : ℝ)
⊢ 0 ≤ 3 * (a ^ n / (↑n : ℝ)) + 4 * (a ^ n * (z ^ n).re / (↑n : ℝ)) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re / (↑n : ℝ)
have inr : ∀ (hn : n > 0),
  0 ≤ 3 * (a ^ n / (↑n : ℝ)) + 4 * (a ^ n * (z ^ n).re / (↑n : ℝ)) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re / (↑n : ℝ)
Tactic: rcases n.eq_zero_or_pos with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * (a ^ n / (↑n : ℝ)) + 4 * (a ^ n * (z ^ n).re / (↑n : ℝ)) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re / (↑n : ℝ)
have inr : 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re) / (↑n : ℝ)
Tactic: simp only [← mul_div_assoc, ← add_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re) / (↑n : ℝ)
have inr : 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re
Tactic: refine div_nonneg ?_ n.cast_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖(↑a : ℂ)‖ < 1
hac₁ : ‖(↑a : ℂ) * z‖ < 1
hac₂ : ‖(↑a : ℂ) * HPow.hPow (β := ℕ) z 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re
have inr : 0 ≤
  3 * a ^ n + 4 * (a ^ n * (z ^ n).re) +
    a ^ n *
      (HPow.hPow (β := ℕ) (z ^ n).re 2 -
        (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 1 n) 2 - HPow.hPow (β := ℕ) (z ^ n).re 2))
Tactic: rw [← pow_mul, pow_mul', sq, mul_re, ← sq, ← sq, ← sq_norm_sub_sq_re, norm_pow, hz]