awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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
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))
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (HPow.hPow (β := ℕ) z 2 ^ n).re

Tactic:
rw [← pow_mul, pow_mul', sq, mul_re, ← sq, ← sq, ← sq_norm_sub_sq_re, norm_pow, hz]

Premises used: Complex.mul_re, norm_pow, Complex.sq_norm_sub_sq_re, sq, pow_mul, pow_mul'
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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 ≤ 2 * a ^ n * HPow.hPow (β := ℕ) ((z ^ n).re + 1) 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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
h :
  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)) =
    2 * a ^ n * HPow.hPow (β := ℕ) ((z ^ n).re + 1) 2
⊢ 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:
convert! (show 0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 by positivity) using 1
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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
⊢ 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)) =
    2 * a ^ n * HPow.hPow (β := ℕ) ((z ^ n).re + 1) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
pos :
  ∀ (hn' : IsUnit (M := ZMod N) (↑n : ZMod N)),
    0 ≤
      3 *
            (-log
                  (1 -
                    HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                      (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ))))).re +
          4 *
            (-log
                  (1 -
                    HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                      (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ)))))).re +
        (-log
              (1 -
                HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
                  HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + 2 * I * (↑y : ℂ))))).re
neg :
  ∀ (hn' : ¬IsUnit (M := ZMod N) (↑n : ZMod N)),
    0 ≤
      3 *
            (-log
                  (1 -
                    HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                      (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ))))).re +
          4 *
            (-log
                  (1 -
                    HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                      (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ)))))).re +
        (-log
              (1 -
                HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
                  HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + 2 * I * (↑y : ℂ))))).re
⊢ 0 ≤
    3 *
          (-log
                (1 -
                  HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                    (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ))))).re +
        4 *
          (-log
                (1 -
                  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                    (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ)))))).re +
      (-log
            (1 -
              HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
                HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + 2 * I * (↑y : ℂ))))).re

Tactic:
by_cases hn' : IsUnit (n : ZMod N)

Premises used: IsUnit, Nat.cast
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
rw : HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ 0 ∨ 1 < HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1

Tactic:
rw [Real.rpow_neg (Nat.cast_nonneg n), inv_lt_one_iff₀]

Premises used: Nat.cast_nonneg, inv_lt_one_iff₀, Real.rpow_neg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ 0 ∨ 1 < HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
.inr <| Real.one_lt_rpow (mod_cast one_lt_two.trans_le hn) <| zero_lt_one.trans hx

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, zero_lt_one, LT.lt.trans_le, LT.lt, LT.lt.trans, one_lt_two, congrFun', Eq.symm, Real.one_lt_rpow, Nat.cast_one, Or.inr, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ 0 ∨ 1 < HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
exact .inr <| Real.one_lt_rpow (mod_cast one_lt_two.trans_le hn) <| zero_lt_one.trans hx

Premises used: zero_lt_one, LT.lt.trans, Real.one_lt_rpow
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1

Tactic:
have hn : (n : ℝ) ^ (-x) < 1 := by
      rw [Real.rpow_neg (Nat.cast_nonneg n), inv_lt_one_iff₀]
      exact .inr <| Real.one_lt_rpow (mod_cast one_lt_two.trans_le hn) <| zero_lt_one.trans hx
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
rw : 1 * HPow.hPow (α := ℝ) (↑n : ℝ) (-(I * (↑y : ℂ))).re = 1
⊢ ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1

Tactic:
rw [norm_mul, ← hn'.unit_spec, DirichletCharacter.unit_norm_eq_one χ hn'.unit,
        ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (mod_cast by lia)]

Premises used: DirichletCharacter.unit_norm_eq_one, norm_mul, Complex.ofReal_natCast, IsUnit.unit, IsUnit.unit_spec, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
⊢ 1 * HPow.hPow (α := ℝ) (↑n : ℝ) (-(I * (↑y : ℂ))).re = 1

Tactic:
simp only [neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self,
        neg_zero, Real.rpow_zero, one_mul]

Premises used: Complex.mul_re, sub_self, MulZeroClass.zero_mul, Real.rpow_zero, Complex.I_re, Complex.I_im, MulZeroClass.mul_zero, Complex.neg_re, Complex.ofReal_re, Complex.ofReal_im, neg_zero, one_mul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
⊢ ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1

Tactic:
have hz : ‖χ n * (n : ℂ) ^ (-(I * y))‖ = 1 := by
      rw [norm_mul, ← hn'.unit_spec, DirichletCharacter.unit_norm_eq_one χ hn'.unit,
        ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (mod_cast by lia)]
      simp only [neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self,
        neg_zero, Real.rpow_zero, one_mul]
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
hz : ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1
pos :
  0 ≤
    3 * (-log (1 - HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ)))).re +
        4 *
          (-log
                (1 -
                  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                    (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ)))))).re +
      (-log
            (1 -
              HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
                HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + 2 * I * (↑y : ℂ))))).re
⊢ 0 ≤
    3 *
          (-log
                (1 -
                  HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                    (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ))))).re +
        4 *
          (-log
                (1 -
                  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                    (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ)))))).re +
      (-log
            (1 -
              HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
                HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + 2 * I * (↑y : ℂ))))).re

Tactic:
rw [MulChar.one_apply hn', one_mul]

Premises used: MulChar.one_apply, one_mul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
hz : ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (-x)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
hz : ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1
h : log (1 - HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ))) = log (1 - (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ))
h₁ :
  log
      (1 -
        HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
          (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ))))) =
    log
      (1 -
        (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
h₂ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + 2 * I * (↑y : ℂ))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
⊢ 0 ≤
    3 * (-log (1 - HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ)))).re +
        4 *
          (-log
                (1 -
                  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                    (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ)))))).re +
      (-log
            (1 -
              HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
                HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + 2 * I * (↑y : ℂ))))).re

Tactic:
convert! re_log_comb_nonneg' (by positivity) hn hz using 6

Premises used: _private.0.DirichletCharacter.re_log_comb_nonneg'
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
hz : ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1
⊢ log (1 - HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ))) = log (1 - (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ))

Tactic:
simp only [ofReal_cpow n.cast_nonneg (-x), ofReal_natCast, ofReal_neg]

Premises used: Nat.cast_nonneg, Complex.ofReal_cpow, Complex.ofReal_neg, Complex.ofReal_natCast, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
hz : ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1
h :
  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
      (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))
⊢ log
      (1 -
        HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
          (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ))))) =
    log
      (1 -
        (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
hz : ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1
⊢ ¬n = 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
hz : ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1
h :
  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
      (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ) + -(I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))
h₁ :
  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
      (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ)) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))
h₂ :
  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
      (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))
h₃ :
  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
      (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))) =
    (↑(↑n : ℝ) : ℂ) ^ (↑(-x) : ℂ) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))
h₄ :
  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
      (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))
h₅ h₆ :
  HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))
⊢ HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
      (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))

Tactic:
rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, mul_left_comm]

Premises used: Nat.cast_nonneg, Complex.ofReal_cpow, Complex.ofReal_neg, neg_add, mul_left_comm, Complex.ofReal_natCast, Complex.cpow_add, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn_1 : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit (M := ZMod N) (↑n : ZMod N)
hn : HPow.hPow (α := ℝ) (↑n : ℝ) (-x) < 1
hz : ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1
⊢ -(2 * I * (↑y : ℂ)) = (↑2 : ℂ) * -(I * (↑y : ℂ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : ¬IsUnit (M := ZMod N) (↑n : ZMod N)
⊢ 0 ≤
    3 *
          (-log
                (1 -
                  HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                    (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ))))).re +
        4 *
          (-log
                (1 -
                  HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ)
                    (HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + I * (↑y : ℂ)))))).re +
      (-log
            (1 -
              HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
                HPow.hPow (α := ℂ) (↑n : ℂ) (-((↑x : ℂ) + 2 * I * (↑y : ℂ))))).re

Tactic:
simp only [MulChar.map_nonunit _ hn', zero_mul, sub_zero, log_one, neg_zero, zero_re, mul_zero,
      neg_add_rev, add_zero, pow_two, le_refl]

Premises used: neg_add_rev, Complex.log_one, le_refl, pow_two, sub_zero, MulZeroClass.zero_mul, MulZeroClass.mul_zero, MulChar.map_nonunit, Complex.zero_re, add_zero, neg_zero
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))‖ ≤
    HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re

Tactic:
simpa only [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs]
      using mul_le_of_le_one_left (by positivity) (χ.norm_le_one _)

Premises used: DirichletCharacter.norm_le_one, norm_mul, mul_le_of_le_one_left, Complex.re_neg_ne_zero_of_one_lt_re, Complex.norm_natCast_cpow_of_re_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ ∀ (p : Nat.Primes),
    ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))‖ ≤
      HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re

Tactic:
have (p : Nat.Primes) : ‖χ p * (p : ℂ) ^ (-s)‖ ≤ (p : ℝ) ^ (-s).re := by
    simpa only [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs]
      using mul_le_of_le_one_left (by positivity) (χ.norm_le_one _)
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this :
  ∀ (p : Nat.Primes),
    ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))‖ ≤
      HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re
⊢ Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))

Tactic:
(Nat.Primes.summable_rpow.mpr ?_).of_nonneg_of_le (fun _ ↦ norm_nonneg _) this
    |>.of_norm.clog_one_sub.neg

Premises used: Iff.mpr, Summable.of_norm, Summable.neg, Summable.of_nonneg_of_le, Summable.clog_one_sub, Nat.Primes.summable_rpow, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this :
  ∀ (p : Nat.Primes),
    ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))‖ ≤
      HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re
refine : (-s).re < -1
⊢ Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))

Tactic:
refine (Nat.Primes.summable_rpow.mpr ?_).of_nonneg_of_le (fun _ ↦ norm_nonneg _) this
    |>.of_norm.clog_one_sub.neg

Premises used: Iff.mpr, Summable.of_norm, Summable.neg, Summable.of_nonneg_of_le, Summable.clog_one_sub, Nat.Primes.summable_rpow, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this :
  ∀ (p : Nat.Primes),
    ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s))‖ ≤
      HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) (-s).re
⊢ (-s).re < -1

Tactic:
simp only [neg_re, neg_lt_neg_iff, hs]

Premises used: neg_lt_neg_iff, Complex.neg_re
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
x : ℝ
hx : 0 < x
y : ℝ
⊢ 1 < (1 + (↑x : ℂ)).re ∧ 1 < (1 + (↑x : ℂ) + I * (↑y : ℂ)).re ∧ 1 < (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)).re

Tactic:
simp only [add_re, one_re, ofReal_re, lt_add_iff_pos_right, hx, mul_re, I_re, zero_mul, I_im,
    ofReal_im, mul_zero, sub_self, add_zero, re_ofNat, im_ofNat, mul_one, mul_im, and_self]

Premises used: Complex.mul_im, lt_add_iff_pos_right, Complex.mul_re, sub_self, and_self, MulZeroClass.zero_mul, Complex.add_re, Complex.I_re, Complex.I_im, MulZeroClass.mul_zero, Complex.re_ofNat, Complex.ofReal_re, Complex.ofReal_im, mul_one, add_zero, Complex.one_re, Complex.im_ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
⊢ 1 < (1 + (↑x : ℂ)).re

Tactic:
have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + (↑x : ℂ)).re
⊢ 1 < (1 + (↑x : ℂ) + I * (↑y : ℂ)).re

Tactic:
have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + (↑x : ℂ)).re
h₁ : 1 < (1 + (↑x : ℂ) + I * (↑y : ℂ)).re
⊢ 1 < (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)).re

Tactic:
have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + (↑x : ℂ)).re
h₁ : 1 < (1 + (↑x : ℂ) + I * (↑y : ℂ)).re
h₂ : 1 < (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)).re
⊢ Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))

Tactic:
have H₀ := summable_neg_log_one_sub_mul_prime_cpow (N := N) 1 h₀