awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
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
⊢ ‖HPow.hPow (β := ℕ) (L (fun (n : ℕ) ↦ (1 : (a : ZMod N) → ℂ) (↑n : ZMod N)) (1 + (↑x : ℂ))) 3 *
          HPow.hPow (β := ℕ) (L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) (1 + (↑x : ℂ) + I * (↑y : ℂ))) 4 *
        L (fun (n : ℕ) ↦ (HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑n : ZMod N)) (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ))‖ ≥
    1
have 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
Tactic: have hsum₁ := (hasSum_re H₁.hasSum).summable.mul_left 4
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
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
⊢ ‖HPow.hPow (β := ℕ) (L (fun (n : ℕ) ↦ (1 : (a : ZMod N) → ℂ) (↑n : ZMod N)) (1 + (↑x : ℂ))) 3 *
          HPow.hPow (β := ℕ) (L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) (1 + (↑x : ℂ) + I * (↑y : ℂ))) 4 *
        L (fun (n : ℕ) ↦ (HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑n : ZMod N)) (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ))‖ ≥
    1
have 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
Tactic: have hsum₂ := (hasSum_re H₂.hasSum).summable
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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
⊢ ‖HPow.hPow (β := ℕ) (L (fun (n : ℕ) ↦ (1 : (a : ZMod N) → ℂ) (↑n : ZMod N)) (1 + (↑x : ℂ))) 3 *
          HPow.hPow (β := ℕ) (L (fun (n : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑n : ZMod N)) (1 + (↑x : ℂ) + I * (↑y : ℂ))) 4 *
        L (fun (n : ℕ) ↦ (HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑n : ZMod N)) (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ))‖ ≥
    1
have rw : ‖HPow.hPow (β := ℕ)
          (cexp
            (∑' (p : Nat.Primes),
              -log
                  (1 -
                    HMul.hMul (α := ℂ) ((1 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
                      (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ)))))))
          3 *
        HPow.hPow (β := ℕ)
          (cexp
            (∑' (p : Nat.Primes),
              -log
                  (1 -
                    HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
                      (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + I * (↑y : ℂ)))))))
          4 *
      cexp
        (∑' (p : Nat.Primes),
          -log
              (1 -
                HMul.hMul (α := ℂ) ((HPow.hPow (β := ℕ) χ 2 : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
                  (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-(1 + (↑x : ℂ) + 2 * I * (↑y : ℂ))))))‖ ≥
  1
Tactic: rw [← LSeries_eulerProduct_exp_log _ h₀, ← LSeries_eulerProduct_exp_log χ h₁,
    ← LSeries_eulerProduct_exp_log _ h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
⊢ ‖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
have h₀ : 1 < (1 + (↑x : ℂ)).re
Tactic: have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + (↑x : ℂ)).re
⊢ ‖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
have h₁ : 1 < (1 + (↑x : ℂ) + I * (↑y : ℂ)).re
Tactic: have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + (↑x : ℂ)).re
h₁ : 1 < (1 + (↑x : ℂ) + I * (↑y : ℂ)).re
⊢ ‖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
have h₂ : 1 < (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ)).re
Tactic: have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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 (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
          HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑y : ℂ))) 4 *
        LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + 2 * I * (↑y : ℂ))‖ ≥
    1
have 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
Tactic: rw [LFunctionTrivChar, DirichletCharacter.LFunction_eq_LSeries 1 h₀,
    χ.LFunction_eq_LSeries h₁, (χ ^ 2).LFunction_eq_LSeries h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
⊢ Tendsto (β := ℂ) (fun (w : ℂ) ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
have h : Eq (α := ℂ → ℂ) (fun (w : ℂ) ↦ w * LFunctionTrivChar N (1 + w))
  ((fun (s : ℂ) ↦ (s - 1) * LFunctionTrivChar N s) ∘ fun (w : ℂ) ↦ 1 + w)
Tactic: convert! (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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)
⊢ Tendsto (β := ℂ) (fun (w : ℂ) ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
    (𝓝 (∏ p ∈ N.primeFactors, HSub.hSub (α := ℂ) 1 (↑p : ℂ)⁻¹))
have convert_2 : Tendsto (β := ℂ) (fun (w : ℂ) ↦ 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)
Tactic: convert! (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
inst : NeZero N
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[≠] 0) (fun (w : ℂ) ↦ LFunctionTrivChar N (1 + w)) fun (x : ℂ) ↦ 1 / x
have H : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
inst : NeZero N
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunctionTrivChar N (1 + (↑x : ℂ))) fun (x : ℝ) ↦ 1 / (↑x : ℂ)
have this : 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 ℂ
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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
have refine : IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ LFunction χ (1 + (↑x : ℂ) + I * (↑y : ℂ))) fun (x : ℝ) ↦ 1
Tactic: refine IsBigO.mono ?_ nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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
have simp_rw : IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ 1
Tactic: simp_rw [add_comm (1 : ℂ), add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ 1
have this : ContinuousAt (LFunction χ) (1 + I * (↑y : ℂ))
Tactic: have := (χ.differentiableAt_LFunction _ <| one_add_I_mul_ne_one_or χ hy).continuousAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (1 + I * (↑y : ℂ))
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ 1
have this₁ : ContinuousAt (LFunction χ) (0 + (1 + I * (↑y : ℂ)))
Tactic: rw [← zero_add (1 + _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * (↑y : ℂ)) = 0
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunction χ (1 + (↑x : ℂ) + I * (↑y : ℂ))) fun (x : ℝ) ↦ (↑x : ℂ)
have simp_rw : IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ (↑x : ℂ)
Tactic: simp_rw [add_comm (1 : ℂ), add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * (↑y : ℂ)) = 0
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ (↑x : ℂ)
have this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (1 + I * (↑y : ℂ))) (1 + I * (↑y : ℂ))
Tactic: have := (χ.differentiableAt_LFunction _ <| one_add_I_mul_ne_one_or χ hy).hasDerivAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
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 : ℂ))
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ LFunction χ ((↑x : ℂ) + (1 + I * (↑y : ℂ)))) fun (x : ℝ) ↦ (↑x : ℂ)
have this₁ : HasDerivAt (LFunction χ) (deriv (LFunction χ) (0 + (1 + I * (↑y : ℂ)))) (0 + (1 + I * (↑y : ℂ)))
Tactic: rw [← zero_add (1 + _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
⊢ t ≠ 0 ∨ χ ≠ 1
have refine : ∀ (h : HPow.hPow (β := ℕ) χ 2 ≠ 1) (H : χ = 1), False
Tactic: refine h.symm.imp_right (fun h H ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
⊢ False
have hz₁ : t ≠ 0 ∨ χ ≠ 1
Tactic: have hz₁ : t ≠ 0 ∨ χ ≠ 1 := by
    refine h.symm.imp_right (fun h H ↦ ?_)
    simp only [H, one_pow, ne_eq, not_true_eq_false] at h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
⊢ False
have hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
Tactic: have hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1 :=
    h.symm.imp_left <| mul_ne_zero two_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
x : ℝ
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
have inl : HPow.hPow (β := ℕ) (1 / (↑0 : ℂ)) 3 * HPow.hPow (β := ℕ) (↑0 : ℂ) 4 * 1 = (↑0 : ℂ)
Tactic: rcases eq_or_ne x 0 with rfl | h
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
x : ℝ
inl : HPow.hPow (β := ℕ) (1 / (↑0 : ℂ)) 3 * HPow.hPow (β := ℕ) (↑0 : ℂ) 4 * 1 = (↑0 : ℂ)
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
have inr : ∀ (h : x ≠ 0), HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
Tactic: rcases eq_or_ne x 0 with rfl | h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
⊢ HPow.hPow (β := ℕ) (1 / (↑0 : ℂ)) 3 * HPow.hPow (β := ℕ) (↑0 : ℂ) 4 * 1 = (↑0 : ℂ)
have inl : HPow.hPow (β := ℕ) (1 / 0) 3 * HPow.hPow (α := ℂ) (β := ℕ) 0 4 * 1 = 0
Tactic: rw [ofReal_zero, zero_pow (by lia), mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
inl : HPow.hPow (β := ℕ) (1 / 0) 3 * HPow.hPow (α := ℂ) (β := ℕ) 0 4 * 1 = 0
⊢ HPow.hPow (β := ℕ) (1 / (↑0 : ℂ)) 3 * HPow.hPow (β := ℕ) (↑0 : ℂ) 4 * 1 = (↑0 : ℂ)
have inl₁ : HPow.hPow (β := ℕ) (1 / 0) 3 * 0 * 1 = 0
Tactic: rw [ofReal_zero, zero_pow (by lia), mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
inl : HPow.hPow (β := ℕ) (1 / 0) 3 * HPow.hPow (α := ℂ) (β := ℕ) 0 4 * 1 = 0
inl₁ : HPow.hPow (β := ℕ) (1 / 0) 3 * 0 * 1 = 0
⊢ HPow.hPow (β := ℕ) (1 / (↑0 : ℂ)) 3 * HPow.hPow (β := ℕ) (↑0 : ℂ) 4 * 1 = (↑0 : ℂ)
have inl₂ : HMul.hMul (α := ℂ) 0 1 = 0
Tactic: rw [ofReal_zero, zero_pow (by lia), mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
inl : HPow.hPow (β := ℕ) (1 / 0) 3 * HPow.hPow (α := ℂ) (β := ℕ) 0 4 * 1 = 0
inl₁ : HPow.hPow (β := ℕ) (1 / 0) 3 * 0 * 1 = 0
inl₂ : HMul.hMul (α := ℂ) 0 1 = 0
⊢ HPow.hPow (β := ℕ) (1 / (↑0 : ℂ)) 3 * HPow.hPow (β := ℕ) (↑0 : ℂ) 4 * 1 = (↑0 : ℂ)
have inl₃ : Eq (α := ℂ) 0 0
Tactic: rw [ofReal_zero, zero_pow (by lia), mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h_1 : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
x : ℝ
h : x ≠ 0
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
have inr : HPow.hPow (β := ℕ) (↑x : ℂ)⁻¹ 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
Tactic: rw [one_div, inv_pow, pow_succ _ 3, ← mul_assoc,
        inv_mul_cancel₀ <| pow_ne_zero 3 (ofReal_ne_zero.mpr h), one_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h_1 : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
x : ℝ
h : x ≠ 0
inr : HPow.hPow (β := ℕ) (↑x : ℂ)⁻¹ 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
have inr₁ : (HPow.hPow (β := ℕ) (↑x : ℂ) 3)⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
Tactic: rw [one_div, inv_pow, pow_succ _ 3, ← mul_assoc,
        inv_mul_cancel₀ <| pow_ne_zero 3 (ofReal_ne_zero.mpr h), one_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h_1 : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
x : ℝ
h : x ≠ 0
inr : HPow.hPow (β := ℕ) (↑x : ℂ)⁻¹ 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
inr₁ : (HPow.hPow (β := ℕ) (↑x : ℂ) 3)⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
have inr₂ : (HPow.hPow (β := ℕ) (↑x : ℂ) 3)⁻¹ * (HPow.hPow (β := ℕ) (↑x : ℂ) 3 * (↑x : ℂ)) * 1 = (↑x : ℂ)
Tactic: rw [one_div, inv_pow, pow_succ _ 3, ← mul_assoc,
        inv_mul_cancel₀ <| pow_ne_zero 3 (ofReal_ne_zero.mpr h), one_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h_1 : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
x : ℝ
h : x ≠ 0
inr : HPow.hPow (β := ℕ) (↑x : ℂ)⁻¹ 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
inr₁ : (HPow.hPow (β := ℕ) (↑x : ℂ) 3)⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
inr₂ : (HPow.hPow (β := ℕ) (↑x : ℂ) 3)⁻¹ * (HPow.hPow (β := ℕ) (↑x : ℂ) 3 * (↑x : ℂ)) * 1 = (↑x : ℂ)
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
have inr₃ : (HPow.hPow (β := ℕ) (↑x : ℂ) 3)⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 3 * (↑x : ℂ) * 1 = (↑x : ℂ)
Tactic: rw [one_div, inv_pow, pow_succ _ 3, ← mul_assoc,
        inv_mul_cancel₀ <| pow_ne_zero 3 (ofReal_ne_zero.mpr h), one_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h_1 : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
x : ℝ
h : x ≠ 0
inr : HPow.hPow (β := ℕ) (↑x : ℂ)⁻¹ 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
inr₁ : (HPow.hPow (β := ℕ) (↑x : ℂ) 3)⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
inr₂ : (HPow.hPow (β := ℕ) (↑x : ℂ) 3)⁻¹ * (HPow.hPow (β := ℕ) (↑x : ℂ) 3 * (↑x : ℂ)) * 1 = (↑x : ℂ)
inr₃ : (HPow.hPow (β := ℕ) (↑x : ℂ) 3)⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 3 * (↑x : ℂ) * 1 = (↑x : ℂ)
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
have inr₄ : 1 * (↑x : ℂ) * 1 = (↑x : ℂ)
Tactic: rw [one_div, inv_pow, pow_succ _ 3, ← mul_assoc,
        inv_mul_cancel₀ <| pow_ne_zero 3 (ofReal_ne_zero.mpr h), one_mul, mul_one]