awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H₀ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))
⊢ Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))

Tactic:
have H₁ := summable_neg_log_one_sub_mul_prime_cpow χ h₁
-- 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
H₀ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))
H₁ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))
⊢ Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)))))

Tactic:
have H₂ := summable_neg_log_one_sub_mul_prime_cpow (χ ^ 2) h₂
-- 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
H₀ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))
H₁ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))
H₂ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)))))
⊢ Summable (α := ℝ) fun (i : Nat.Primes) ↦
    3 *
      (-log
            (1 -
              HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑i : ℕ) : ZMod N) : ℂ)
                (HPow.hPow (α := ℂ) (↑(↑i : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))).re

Tactic:
have hsum₀ := (hasSum_re H₀.hasSum).summable.mul_left 3
-- 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
H₀ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))
H₁ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))
H₂ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)))))
hsum₀ :
  Summable (α := ℝ) fun (i : Nat.Primes) ↦
    3 *
      (-log
            (1 -
              HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑i : ℕ) : ZMod N) : ℂ)
                (HPow.hPow (α := ℂ) (↑(↑i : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))).re
⊢ Summable (α := ℝ) fun (i : Nat.Primes) ↦
    4 *
      (-log
            (1 -
              HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑i : ℕ) : ZMod N) : ℂ)
                (HPow.hPow (α := ℂ) (↑(↑i : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))).re

Tactic:
have hsum₁ := (hasSum_re H₁.hasSum).summable.mul_left 4
-- 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
H₀ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))
H₁ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))
H₂ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)))))
hsum₀ :
  Summable (α := ℝ) fun (i : Nat.Primes) ↦
    3 *
      (-log
            (1 -
              HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑i : ℕ) : ZMod N) : ℂ)
                (HPow.hPow (α := ℂ) (↑(↑i : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))).re
hsum₁ :
  Summable (α := ℝ) fun (i : Nat.Primes) ↦
    4 *
      (-log
            (1 -
              HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑i : ℕ) : ZMod N) : ℂ)
                (HPow.hPow (α := ℂ) (↑(↑i : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))).re
⊢ Summable (α := ℝ) fun (x_1 : Nat.Primes) ↦
    (-log
          (1 -
            HMul.hMul (α := ℂ) ((HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑(↑x_1 : ℕ) : ZMod N) : ℂ)
              (HPow.hPow (α := ℂ) (↑(↑x_1 : ℕ) : ℂ) (-(1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)))))).re

Tactic:
have hsum₂ := (hasSum_re H₂.hasSum).summable
-- 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
H₀ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))
H₁ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))
H₂ :
  Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)))))
hsum₀ :
  Summable (α := ℝ) fun (i : Nat.Primes) ↦
    3 *
      (-log
            (1 -
              HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑i : ℕ) : ZMod N) : ℂ)
                (HPow.hPow (α := ℂ) (↑(↑i : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))).re
hsum₁ :
  Summable (α := ℝ) fun (i : Nat.Primes) ↦
    4 *
      (-log
            (1 -
              HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑i : ℕ) : ZMod N) : ℂ)
                (HPow.hPow (α := ℂ) (↑(↑i : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))).re
hsum₂ :
  Summable (α := ℝ) fun (x_1 : Nat.Primes) ↦
    (-log
          (1 -
            HMul.hMul (α := ℂ) ((HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑(↑x_1 : ℕ) : ZMod N) : ℂ)
              (HPow.hPow (α := ℂ) (↑(↑x_1 : ℕ) : ℂ) (-(1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)))))).re
⊢ LE.le (α := ℝ) 0
    (∑' (b : Nat.Primes),
      (3 *
            (-log
                  (1 -
                    HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑b : ℕ) : ZMod N) : ℂ)
                      (HPow.hPow (α := ℂ) (↑(↑b : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))).re +
          4 *
            (-log
                  (1 -
                    HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑b : ℕ) : ZMod N) : ℂ)
                      (HPow.hPow (α := ℂ) (↑(↑b : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))).re +
        (-log
              (1 -
                HMul.hMul (α := ℂ) ((HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑(↑b : ℕ) : ZMod N) : ℂ)
                  (HPow.hPow (α := ℂ) (↑(↑b : ℕ) : ℂ) (-(1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)))))).re))

Tactic:
simpa only [neg_add_rev, neg_re, mul_neg, χ.pow_apply' two_ne_zero, ge_iff_le, add_re, one_re,
    ofReal_re, ofReal_add, ofReal_one] using
      tsum_nonneg fun (p : Nat.Primes) ↦ χ.re_log_comb_nonneg p.prop.two_le h₀ y

Premises used: neg_add_rev, ge_iff_le, Complex.ofReal_add, Complex.add_re, Complex.ofReal_one, MulChar.pow_apply', two_ne_zero, Subtype.prop, Complex.neg_re, Nat.Prime.two_le, Complex.ofReal_re, tsum_nonneg, Complex.one_re, _private.0.DirichletCharacter.re_log_comb_nonneg, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero 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
inst : NeZero 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
inst : NeZero 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
inst : NeZero 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
rw :
  ‖HPow.hPow (β := ℕ) (LSeries (fun (x : ℕ) ↦ (1 : (a : ZMod N) → ℂ) (↑x : ZMod N)) (1 + (↑x : ℂ))) 3 *
          HPow.hPow (β := ℕ)
            (LSeries (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) (1 + (↑x : ℂ) + I * (↑y : ℂ))) 4 *
        LSeries (fun (x : ℕ) ↦ (HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑x : ZMod N))
          (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ))‖ ≥
    1
⊢ ‖HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
          HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑y : ℂ))) 4 *
        LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ))‖ ≥
    1

Tactic:
rw [LFunctionTrivChar, DirichletCharacter.LFunction_eq_LSeries 1 h₀,
    χ.LFunction_eq_LSeries h₁, (χ ^ 2).LFunction_eq_LSeries h₂]

Premises used: DirichletCharacter.LFunction_eq_LSeries, HPow.hPow, DirichletCharacter.LFunctionTrivChar, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero 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
⊢ ‖HPow.hPow (β := ℕ) (LSeries (fun (x : ℕ) ↦ (1 : (a : ZMod N) → ℂ) (↑x : ZMod N)) (1 + (↑x : ℂ))) 3 *
          HPow.hPow (β := ℕ)
            (LSeries (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) (1 + (↑x : ℂ) + I * (↑y : ℂ))) 4 *
        LSeries (fun (x : ℕ) ↦ (HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑x : ZMod N))
          (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ))‖ ≥
    1

Tactic:
norm_LSeries_product_ge_one χ hx y

Premises used: DirichletCharacter.norm_LSeries_product_ge_one
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero 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
⊢ ‖HPow.hPow (β := ℕ) (LSeries (fun (x : ℕ) ↦ (1 : (a : ZMod N) → ℂ) (↑x : ZMod N)) (1 + (↑x : ℂ))) 3 *
          HPow.hPow (β := ℕ)
            (LSeries (fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) (1 + (↑x : ℂ) + I * (↑y : ℂ))) 4 *
        LSeries (fun (x : ℕ) ↦ (HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑x : ZMod N))
          (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ))‖ ≥
    1

Tactic:
exact norm_LSeries_product_ge_one χ hx y

Premises used: DirichletCharacter.norm_LSeries_product_ge_one
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
⊢ Tendsto (α := ℂ) (β := ℂ) ((fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) ∘ fun (w : ℂ) ↦ 1 + w) (𝓝[≠] 0)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))

Tactic:
(LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_

Premises used: DirichletCharacter.LFunctionTrivChar_residue_one, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
h :
  Eq (α := ℂ → ℂ) (fun (w : ℂ) ↦ w * LFunctionTrivChar N (1 + w))
    ((fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) ∘ fun (w : ℂ) ↦ 1 + w)
convert_2 : Tendsto (β := ℂ) (fun (w : ℂ) ↦ 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)
⊢ Tendsto (β := ℂ) (fun (w : ℂ) ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))

Tactic:
convert! (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1

Premises used: DirichletCharacter.LFunctionTrivChar_residue_one, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
⊢ Eq (α := ℂ → ℂ) (fun (w : ℂ) ↦ w * LFunctionTrivChar N (1 + w))
    ((fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) ∘ fun (w : ℂ) ↦ 1 + w)

Tactic:
simp only [Function.comp_def, add_sub_cancel_left]

Premises used: add_sub_cancel_left, Function.comp_def
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
⊢ Tendsto (β := ℂ) (fun (w : ℂ) ↦ 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)

Tactic:
simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
          ((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le

Premises used: Homeomorph.coe_addLeft, Homeomorph.map_punctured_nhds_eq, Eq.le, Filter.tendsto_iff_comap, Homeomorph.addLeft, Filter.map_le_iff_le_comap, add_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
⊢ Tendsto (β := ℂ) (fun (w : ℂ) ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))

Tactic:
have H : Tendsto (fun w ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
        (𝓝 <| ∏ p ∈ N.primeFactors, (1 - (p : ℂ)⁻¹)) := by
      convert! (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1
      · simp only [Function.comp_def, add_sub_cancel_left]
      · simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
          ((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
H :
  Tendsto (β := ℂ) (fun (w : ℂ) ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (w : ℂ) ↦ LFunctionTrivChar N (1 + w)) fun (x : ℂ) ↦ 1 / x

Tactic:
(isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <| H.isBigO_one ℂ

Premises used: Filter.Tendsto.isBigO_one, eventually_mem_nhdsWithin, Set.Mem, setOf, Asymptotics.isBigO_mul_iff_isBigO_div, Set.singleton, Iff.mp, Complex, Not
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
H :
  Tendsto (β := ℂ) (fun (w : ℂ) ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (w : ℂ) ↦ LFunctionTrivChar N (1 + w)) fun (x : ℂ) ↦ 1 / x

Tactic:
exact (isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <| H.isBigO_one ℂ

Premises used: Filter.Tendsto.isBigO_one, eventually_mem_nhdsWithin, Asymptotics.isBigO_mul_iff_isBigO_div, Iff.mp, Complex
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (w : ℂ) ↦ LFunctionTrivChar N (1 + w)) fun (x : ℂ) ↦ 1 / x

Tactic:
have : (fun w : ℂ ↦ LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] (1 / ·) := by
    have H : Tendsto (fun w ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
        (𝓝 <| ∏ p ∈ N.primeFactors, (1 - (p : ℂ)⁻¹)) := by
      convert! (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1
      · simp only [Function.comp_def, add_sub_cancel_left]
      · simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
          ((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le
    exact (isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <| H.isBigO_one ℂ
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
this : IsBigO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (w : ℂ) ↦ LFunctionTrivChar N (1 + w)) fun (x : ℂ) ↦ 1 / x
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunctionTrivChar N (1 + (↑x : ℂ))) fun (x : ℝ) ↦ 1 / (↑x : ℂ)

Tactic:
(isBigO_comp_ofReal_nhds_ne this).mono <| nhdsGT_le_nhdsNE 0

Premises used: nhdsGT_le_nhdsNE, Complex.isBigO_comp_ofReal_nhds_ne, Asymptotics.IsBigO.mono, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
this : IsBigO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (w : ℂ) ↦ LFunctionTrivChar N (1 + w)) fun (x : ℂ) ↦ 1 / x
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunctionTrivChar N (1 + (↑x : ℂ))) fun (x : ℝ) ↦ 1 / (↑x : ℂ)

Tactic:
exact (isBigO_comp_ofReal_nhds_ne this).mono <| nhdsGT_le_nhdsNE 0

Premises used: nhdsGT_le_nhdsNE, Complex.isBigO_comp_ofReal_nhds_ne, Asymptotics.IsBigO.mono, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ 1 + I * (↑y : ℂ) ≠ 1 ∨ χ ≠ 1

Tactic:
simpa only [ne_eq, add_eq_left, _root_.mul_eq_zero, I_ne_zero, ofReal_eq_zero, false_or]
    using hy

Premises used: Complex.I_ne_zero, false_or, mul_eq_zero, ne_eq, Complex.ofReal_eq_zero, add_eq_left
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunction χ (1 + (↑x : ℂ) + I * (↑y : ℂ))) fun (x : ℝ) ↦ 1

Tactic:
IsBigO.mono ?_ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Asymptotics.IsBigO.mono
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
refine : IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ LFunction χ (1 + (↑x : ℂ) + I * (↑y : ℂ))) fun (x : ℝ) ↦ 1
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunction χ (1 + (↑x : ℂ) + I * (↑y : ℂ))) fun (x : ℝ) ↦ 1

Tactic:
refine IsBigO.mono ?_ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Asymptotics.IsBigO.mono
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
simp_rw : IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ 1
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ LFunction χ (1 + (↑x : ℂ) + I * (↑y : ℂ))) fun (x : ℝ) ↦ 1

Tactic:
simp_rw [add_comm (1 : ℂ), add_assoc]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ ContinuousAt (LFunction χ) (1 + I * (↑y : ℂ))

Tactic:
have := (χ.differentiableAt_LFunction _ <| one_add_I_mul_ne_one_or χ hy).continuousAt
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (1 + I * (↑y : ℂ))
⊢ ContinuousAt (LFunction χ) (0 + (1 + I * (↑y : ℂ)))

Tactic:
rw [← zero_add (1 + _)] at this

Premises used: zero_add, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * (↑y : ℂ)))
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) + (1 + I * (↑y : ℂ))) 0

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * (↑y : ℂ)))
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ 1

Tactic:
exact this.comp (f := fun x : ℝ ↦ x + (1 + I * y)) (x := 0) (by fun_prop) |>.tendsto.isBigO_one ℂ

Premises used: Filter.Tendsto.isBigO_one, ContinuousAt.tendsto, ContinuousAt.comp, Complex
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * (↑y : ℂ)) = 0
simp_rw :
  IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ (↑x : ℂ)
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunction χ (1 + (↑x : ℂ) + I * (↑y : ℂ))) fun (x : ℝ) ↦ (↑x : ℂ)

Tactic:
simp_rw [add_comm (1 : ℂ), add_assoc]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * (↑y : ℂ)) = 0
⊢ HasDerivAt (LFunction χ) (deriv (LFunction χ) (1 + I * (↑y : ℂ))) (1 + I * (↑y : ℂ))

Tactic:
have := (χ.differentiableAt_LFunction _ <| one_add_I_mul_ne_one_or χ hy).hasDerivAt
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * (↑y : ℂ)) = 0
this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (1 + I * (↑y : ℂ))) (1 + I * (↑y : ℂ))
⊢ HasDerivAt (LFunction χ) (deriv (LFunction χ) (0 + (1 + I * (↑y : ℂ)))) (0 + (1 + I * (↑y : ℂ)))

Tactic:
rw [← zero_add (1 + _)] at this

Premises used: zero_add, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * (↑y : ℂ)) = 0
this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (0 + (1 + I * (↑y : ℂ)))) (0 + (1 + I * (↑y : ℂ)))
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ (↑x : ℂ)

Tactic:
simpa only [zero_add, h, sub_zero]
    using (Complex.isBigO_comp_ofReal_nhds
      (this.comp_add_const 0 _).differentiableAt.isBigO_sub) |>.mono nhdsWithin_le_nhds

Premises used: sub_zero, HasDerivAt.differentiableAt, zero_add, DifferentiableAt.isBigO_sub, nhdsWithin_le_nhds, Asymptotics.IsBigO.mono, Complex.isBigO_comp_ofReal_nhds, OfNat.ofNat, HasDerivAt.comp_add_const
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
⊢ t ≠ 0 ∨ χ ≠ 1

Tactic:
h.symm.imp_right (fun h H ↦ ?_)

Premises used: Or.symm, Or.imp_right
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
refine : ∀ (h : HPow.hPow (β := ℕ) χ 2 ≠ 1) (H : χ = 1), False
⊢ t ≠ 0 ∨ χ ≠ 1

Tactic:
refine h.symm.imp_right (fun h H ↦ ?_)

Premises used: Or.symm, Or.imp_right
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h_1 : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
h : HPow.hPow (β := ℕ) χ 2 ≠ 1
H : χ = 1
⊢ False

Tactic:
simp only [H, one_pow, ne_eq, not_true_eq_false] at h

Premises used: one_pow, not_true_eq_false, ne_eq