awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : ℕ
χ : DirichletCharacter R n_1
f g : ℕ → R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑x.1 : ZMod n_1) : R) (f x.1) *
        HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑x.2 : ZMod n_1) : R) (g x.2))
    (∑ i ∈ n.divisorsAntidiagonal, HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑n : ZMod n_1) : R) (f i.1 * g i.2))
have h : ∀ (p : ℕ × ℕ) (hp : p ∈ n.divisorsAntidiagonal),
  HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R) (f p.1) *
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) (g p.2) =
    HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑n : ZMod n_1) : R) (f p.1 * g p.2)
Tactic: refine Finset.sum_congr rfl fun p hp ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : ℕ
χ : DirichletCharacter R n_1
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R) (f p.1) *
      HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) (g p.2) =
    HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑n : ZMod n_1) : R) (f p.1 * g p.2)
have h : HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R) (f p.1) *
    HMul.hMul (α := R) ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) (g p.2) =
  HMul.hMul (α := R) (β := R) ((χ : (a : ZMod n_1) → R) (↑p.1 : ZMod n_1) : R)
      ((χ : (a : ZMod n_1) → R) (↑p.2 : ZMod n_1) : R) *
    (f p.1 * g p.2)
Tactic: rw [(mem_divisorsAntidiagonal.mp hp).1.symm, cast_mul, map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ Eq (α := ℂ) ((χ : (a : ZMod n) → ℂ) (↑1 : ZMod n) : ℂ) (1 : ℂ)
have rw : Eq (α := ℂ) ((χ : (a : ZMod n) → ℂ) 1 : ℂ) (1 : ℂ)
Tactic: rw [cast_one, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
rw : Eq (α := ℂ) ((χ : (a : ZMod n) → ℂ) 1 : ℂ) (1 : ℂ)
⊢ Eq (α := ℂ) ((χ : (a : ZMod n) → ℂ) (↑1 : ZMod n) : ℂ) (1 : ℂ)
have rw₁ : Eq (α := ℂ) 1 1
Tactic: rw [cast_one, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ (1 ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ)) = δ
have rw : Eq (α := ℕ → ℂ) ((fun (x : ℕ) ↦ (↑((zeta : (a : ℕ) → ℕ) x) : ℂ)) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
  fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
Tactic: rw [one_convolution_eq_zeta_convolution, ← one_eq_delta]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ Eq (α := ℕ → ℂ) ((fun (x : ℕ) ↦ (↑((zeta : (a : ℕ) → ℕ) x) : ℂ)) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
have simp_rw : Eq (α := ℕ → ℂ)
  ((fun (x : ℕ) ↦ ((↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
  fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
Tactic: simp_rw [← natCoe_apply, ← intCoe_apply, coe_mul, coe_zeta_mul_coe_moebius]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
simp_rw :
  Eq (α := ℕ → ℂ)
    ((fun (x : ℕ) ↦ ((↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
⊢ Eq (α := ℕ → ℂ) ((fun (x : ℕ) ↦ (↑((zeta : (a : ℕ) → ℕ) x) : ℂ)) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
have simp_rw₁ : Eq (α := ℕ → ℂ)
  ((fun (x : ℕ) ↦ ((↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x) ⍟ fun (x : ℕ) ↦
    ((↑μ : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x)
  fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
Tactic: simp_rw [← natCoe_apply, ← intCoe_apply, coe_mul, coe_zeta_mul_coe_moebius]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
simp_rw :
  Eq (α := ℕ → ℂ)
    ((fun (x : ℕ) ↦ ((↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
simp_rw₁ :
  Eq (α := ℕ → ℂ)
    ((fun (x : ℕ) ↦ ((↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x) ⍟ fun (x : ℕ) ↦
      ((↑μ : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) x)
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
⊢ Eq (α := ℕ → ℂ) ((fun (x : ℕ) ↦ (↑((zeta : (a : ℕ) → ℕ) x) : ℂ)) ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ))
    fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
have simp_rw₂ : Eq (α := ℕ → ℂ)
  (⇑(HMul.hMul (α := ArithmeticFunction ℂ) (↑zeta : ArithmeticFunction ℂ) (↑μ : ArithmeticFunction ℂ)) : (a : ℕ) → ℂ)
  fun (n : ℕ) ↦ (1 : (a : ℕ) → ℂ) n
Tactic: simp_rw [← natCoe_apply, ← intCoe_apply, coe_mul, coe_zeta_mul_coe_moebius]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (hypothesis)
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ ((fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) ⍟
      HMul.hMul (α := ℕ → ℂ) (fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) fun (n : ℕ) ↦
        (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) =
    δ
have this : (1 ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ)) = δ
Tactic: have : (1 : ℕ → ℂ) ⍟ (μ ·) = δ := by
    rw [one_convolution_eq_zeta_convolution, ← one_eq_delta]
    simp_rw [← natCoe_apply, ← intCoe_apply, coe_mul, coe_zeta_mul_coe_moebius]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun (x : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) x) : ℂ)) = δ
⊢ ((fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) ⍟
      HMul.hMul (α := ℕ → ℂ) (fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) fun (n : ℕ) ↦
        (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) =
    δ
have nth_rewrite : (HMul.hMul (α := ℕ → ℂ) (fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) 1 ⍟
    HMul.hMul (α := ℕ → ℂ) (fun (n_1 : ℕ) ↦ (χ : (a : ZMod n) → ℂ) (↑n_1 : ZMod n)) fun (n : ℕ) ↦
      (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) =
  δ
Tactic: nth_rewrite 1 [← mul_one ↗χ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
χ : DirichletCharacter ℂ 0
⊢ (fun (n : ℕ) ↦ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0)) = δ
have h : ∀ (n : ℕ), (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
χ : DirichletCharacter ℂ 0
n : ℕ
⊢ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
have h : (χ : (a : ZMod 0) → ℂ) (↑0 : ZMod 0) = δ 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
χ : DirichletCharacter ℂ 0
n : ℕ
h : (χ : (a : ZMod 0) → ℂ) (↑0 : ZMod 0) = δ 0
⊢ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
have h₁ : ∀ (hn : n ≠ 0), (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
χ : DirichletCharacter ℂ 0
⊢ (χ : (a : ZMod 0) → ℂ) (↑0 : ZMod 0) = δ 0
have h : (χ : (a : ZMod 0) → ℂ) 0 = δ 0
Tactic: simp_rw [cast_zero, χ.map_nonunit not_isUnit_zero, delta, reduceCtorEq, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
χ : DirichletCharacter ℂ 0
h : (χ : (a : ZMod 0) → ℂ) 0 = δ 0
⊢ (χ : (a : ZMod 0) → ℂ) (↑0 : ZMod 0) = δ 0
have h₁ : 0 = δ 0
Tactic: simp_rw [cast_zero, χ.map_nonunit not_isUnit_zero, delta, reduceCtorEq, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
χ : DirichletCharacter ℂ 0
h : (χ : (a : ZMod 0) → ℂ) 0 = δ 0
h₁ : 0 = δ 0
⊢ (χ : (a : ZMod 0) → ℂ) (↑0 : ZMod 0) = δ 0
have h₂ : Eq (α := ℂ) 0 (if Eq (α := ℕ) 0 1 then 1 else 0)
Tactic: simp_rw [cast_zero, χ.map_nonunit not_isUnit_zero, delta, reduceCtorEq, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
χ : DirichletCharacter ℂ 0
h : (χ : (a : ZMod 0) → ℂ) 0 = δ 0
h₁ : 0 = δ 0
h₂ : Eq (α := ℂ) 0 (if Eq (α := ℕ) 0 1 then 1 else 0)
⊢ (χ : (a : ZMod 0) → ℂ) (↑0 : ZMod 0) = δ 0
have h₃ : Eq (α := ℂ) 0 (if False then 1 else 0)
Tactic: simp_rw [cast_zero, χ.map_nonunit not_isUnit_zero, delta, reduceCtorEq, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
⊢ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
have h : ∀ (hn : Ne (α := ℕ) 1 0), (χ : (a : ZMod 0) → ℂ) (↑1 : ZMod 0) = δ 1
Tactic: rcases eq_or_ne n 1 with rfl | hn'
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
h : ∀ (hn : Ne (α := ℕ) 1 0), (χ : (a : ZMod 0) → ℂ) (↑1 : ZMod 0) = δ 1
⊢ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
have h₁ : ∀ (hn' : n ≠ 1), (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
Tactic: rcases eq_or_ne n 1 with rfl | hn'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (hypothesis)
Goal:
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
⊢ (χ : (a : ZMod 0) → ℂ) (↑n : ZMod 0) = δ n
have this : ¬IsUnit (M := ZMod 0) (↑n : ZMod 0)
Tactic: have : ¬ IsUnit (n : ZMod 0) := fun h ↦ hn' <| ZMod.eq_one_of_isUnit_natCast h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
⊢ Eq.{u_1 + 1} (α := ℕ → R) (fun (x : ℕ) ↦ (χ : (a : ZMod 1) → R) (↑x : ZMod 1)) 1
have h : ∀ (x : ℕ), Eq (α := R) ((χ : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
x : ℕ
⊢ Eq (α := R) ((χ : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)
have h : Eq.{u_1 + 1} (α := R) ((1 : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)
Tactic: rw [χ.level_one, MulChar.one_apply (isUnit_of_subsingleton _), Pi.one_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
x : ℕ
h : Eq.{u_1 + 1} (α := R) ((1 : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)
⊢ Eq (α := R) ((χ : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)
have h₁ : Eq.{u_1 + 1} (α := R) 1 (1 x)
Tactic: rw [χ.level_one, MulChar.one_apply (isUnit_of_subsingleton _), Pi.one_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
χ : DirichletCharacter R 1
x : ℕ
h : Eq.{u_1 + 1} (α := R) ((1 : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)
h₁ : Eq.{u_1 + 1} (α := R) 1 (1 x)
⊢ Eq (α := R) ((χ : (a : ZMod 1) → R) (↑x : ZMod 1) : R) (1 x : R)
have h₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [χ.level_one, MulChar.one_apply (isUnit_of_subsingleton _), Pi.one_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ ¬LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
have refine : ∀ (h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1),
  Summable (α := ℝ)
    (Set.indicator {n : ℕ | Eq (α := ZMod N) (↑n : ZMod N) 1} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: refine fun h ↦ (Real.not_summable_indicator_one_div_natCast hN 1) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
⊢ Summable (α := ℝ)
    (Set.indicator {n : ℕ | Eq (α := ZMod N) (↑n : ZMod N) 1} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have refine : ∀ (n : ℕ),
  Set.indicator {n : ℕ | Eq (α := ZMod N) (↑n : ZMod N) 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n ≤
    ‖term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1 n‖
Tactic: refine h.norm.of_nonneg_of_le (fun m ↦ Set.indicator_apply_nonneg (fun _ ↦ by positivity))
    (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
⊢ Set.indicator {n : ℕ | Eq (α := ZMod N) (↑n : ZMod N) 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n ≤
    ‖term (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1 n‖
have simp : (if Eq (α := ZMod N) (↑n : ZMod N) 1 then HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) else 0) ≤
  if n = 0 then 0 else norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
Tactic: simp only [norm_term_eq, Set.indicator, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
⊢ (if Eq (α := ZMod N) (↑n : ZMod N) 1 then HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) else 0) ≤
    if n = 0 then 0 else norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
have pos : ∀ (h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1) (h₂ : n = 0), HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ 0
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
pos : ∀ (h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1) (h₂ : n = 0), HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ 0
⊢ (if Eq (α := ZMod N) (↑n : ZMod N) 1 then HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) else 0) ≤
    if n = 0 then 0 else norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
have neg : ∀ (h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1) (h₂ : ¬n = 0),
  HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
    norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
pos : ∀ (h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1) (h₂ : n = 0), HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ 0
neg :
  ∀ (h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1) (h₂ : ¬n = 0),
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
      norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
⊢ (if Eq (α := ZMod N) (↑n : ZMod N) 1 then HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) else 0) ≤
    if n = 0 then 0 else norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
have pos₁ : ∀ (h₁ : ¬Eq (α := ZMod N) (↑n : ZMod N) 1), n = 0 → LE.le (α := ℝ) 0 0
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) 1
n : ℕ
pos : ∀ (h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1) (h₂ : n = 0), HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ 0
neg :
  ∀ (h₁ : Eq (α := ZMod N) (↑n : ZMod N) 1) (h₂ : ¬n = 0),
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
      norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
pos₁ : ∀ (h₁ : ¬Eq (α := ZMod N) (↑n : ZMod N) 1), n = 0 → LE.le (α := ℝ) 0 0
⊢ (if Eq (α := ZMod N) (↑n : ZMod N) 1 then HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) else 0) ≤
    if n = 0 then 0 else norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
have neg₁ : ∀ (h₁ : ¬Eq (α := ZMod N) (↑n : ZMod N) 1),
  ¬n = 0 → 0 ≤ norm (E := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) / HPow.hPow (α := ℝ) (↑n : ℝ) (re 1)
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
⊢ LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s ↔ 1 < s.re
have refine : ∀ (H : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s), 1 < s.re
Tactic: refine ⟨fun H ↦ ?_, LSeriesSummable_of_one_lt_re χ⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s
⊢ 1 < s.re
have by_contra! : ∀ (h : s.re ≤ 1), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ LSeriesSummable ((fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) * f) s
have refine : ∀ (n : ℕ), ‖HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) f n‖ ≤ ‖f n‖
Tactic: refine .of_norm <| h.norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) fun n ↦ norm_term_le s ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s *
      L
        (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
        s =
    1
have rw : L
    ((fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) ⍟
      HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
        (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
    s =
  1
Tactic: rw [← LSeries_convolution' (LSeriesSummable_of_one_lt_re χ hs) <|
          LSeriesSummable_mul χ <| ArithmeticFunction.LSeriesSummable_moebius_iff.mpr hs,
    convolution_mul_moebius, LSeries_delta, Pi.one_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
rw :
  L
      ((fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) ⍟
        HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
      s =
    1
⊢ L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s *
      L
        (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
        s =
    1
have rw₁ : L δ s = 1
Tactic: rw [← LSeries_convolution' (LSeriesSummable_of_one_lt_re χ hs) <|
          LSeriesSummable_mul χ <| ArithmeticFunction.LSeriesSummable_moebius_iff.mpr hs,
    convolution_mul_moebius, LSeries_delta, Pi.one_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
rw :
  L
      ((fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) ⍟
        HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
      s =
    1
rw₁ : L δ s = 1
⊢ L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s *
      L
        (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
        s =
    1
have rw₂ : Eq (α := ℂ) (1 s) 1
Tactic: rw [← LSeries_convolution' (LSeriesSummable_of_one_lt_re χ hs) <|
          LSeriesSummable_mul χ <| ArithmeticFunction.LSeriesSummable_moebius_iff.mpr hs,
    convolution_mul_moebius, LSeries_delta, Pi.one_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
rw :
  L
      ((fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) ⍟
        HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
      s =
    1
rw₁ : L δ s = 1
rw₂ : Eq (α := ℂ) (1 s) 1
⊢ L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) s *
      L
        (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) fun (n : ℕ) ↦
          (↑((μ : (a : ℕ) → ℤ) n) : ℂ))
        s =
    1
have rw₃ : Eq (α := ℂ) 1 1
Tactic: rw [← LSeries_convolution' (LSeriesSummable_of_one_lt_re χ hs) <|
          LSeriesSummable_mul χ <| ArithmeticFunction.LSeriesSummable_moebius_iff.mpr hs,
    convolution_mul_moebius, LSeries_delta, Pi.one_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
⊢ (L fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) = L 1
have h : ∀ (s : ℂ), L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s = L 1 s
Tactic: ext s
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) = 1
have rw : abscissaOfAbsConv 1 = 1
Tactic: rw [abscissaOfAbsConv_congr (g := 1) fun hn ↦ by simp [hn], abscissaOfAbsConv_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
rw : abscissaOfAbsConv 1 = 1
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) = 1
have rw₁ : Eq (α := EReal) 1 1
Tactic: rw [abscissaOfAbsConv_congr (g := 1) fun hn ↦ by simp [hn], abscissaOfAbsConv_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s = riemannZeta s
have suffices : Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n)
  (∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s)
Tactic: suffices ∑' n, term (fun n ↦ if n = 0 then 0 else 1) s n = ∑' n : ℕ, 1 / (n : ℂ) ^ s by
    simpa [LSeries, zeta_eq_tsum_one_div_nat_cpow hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n)
    (∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s)
have refine : ∀ (n : ℕ), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: refine tsum_congr fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
have inl : ∀ (hn : n = 0), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
n : ℕ
inl : ∀ (hn : n = 0), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
have inr : ∀ (hn : n ≠ 0), term (fun (n : ℕ) ↦ if n = 0 then 0 else 1) s n = 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
s : ℂ
hs : 1 < s.re
⊢ L (fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) s * L (fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s = 1
have rw : L ((fun (x : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) x) : ℂ)) ⍟ fun (n : ℕ) ↦ (↑((μ : (a : ℕ) → ℤ) n) : ℂ)) s = 1
Tactic: rw [← LSeries_convolution' (LSeriesSummable_zeta_iff.mpr hs)
    (LSeriesSummable_moebius_iff.mpr hs)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (hypothesis)
Goal:
x : ℝ
hx : 1 < x
⊢ 0 < riemannZeta (↑x : ℂ)
have hx' : 1 < (↑x : ℂ).re
Tactic: have hx' : 1 < (x : ℂ).re := by simpa using hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x : ℂ).re
⊢ 0 < riemannZeta (↑x : ℂ)
have rw : 0 < L 1 (↑x : ℂ)
Tactic: rw [← LSeries_one_eq_riemannZeta hx']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x : ℂ).re
⊢ 0 < L 1 (↑x : ℂ)
have refine : abscissaOfAbsConv 1 < (↑x : EReal)
Tactic: refine LSeries.positive (fun _ ↦ by simp) (by simp) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x : ℂ).re
⊢ abscissaOfAbsConv 1 < (↑x : EReal)
have simpa : 1 < (↑x : EReal)
Tactic: simpa [LSeries.abscissaOfAbsConv_one] using (by exact_mod_cast hx : (1 : EReal) < x)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Dirichlet (goal)
Goal:
⊢ Eq (α := ℕ → ℂ) ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟ fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ))
    fun (n : ℕ) ↦ Complex.log (↑n : ℂ)
have h : ∀ (n : ℕ),
  ((fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) ⍟ fun (n : ℕ) ↦ (↑((ζ : (a : ℕ) → ℕ) n) : ℂ)) n = Complex.log (↑n : ℂ)
Tactic: ext n