awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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 : ℂ))))
⊢ 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 : ℂ))))
have 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 : ℂ))))
Tactic: rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, mul_left_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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
⊢ 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
have 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
Tactic: rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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 :
  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
⊢ 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
have h₁ : HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
    (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ)) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
  (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))) 2
Tactic: rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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 :
  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
h₁ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ)) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
⊢ 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
have h₂ : HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
    (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
  (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))) 2
Tactic: rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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 :
  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
h₁ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ)) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
h₂ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
⊢ 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
have h₃ : HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
    (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
  (↑(↑n : ℝ) : ℂ) ^ (↑(-x) : ℂ) *
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))) 2
Tactic: rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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 :
  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
h₁ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ)) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
h₂ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
h₃ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    (↑(↑n : ℝ) : ℂ) ^ (↑(-x) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
⊢ 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
have h₄ : HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
    (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
  HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) *
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))) 2
Tactic: rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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 :
  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
h₁ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ)) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
h₂ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
h₃ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    (↑(↑n : ℝ) : ℂ) ^ (↑(-x) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
h₄ :
  HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
      (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-(2 * I * (↑y : ℂ)))) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ)))))
        2
⊢ 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
have h₅ : HPow.hPow (α := ℂ) (β := ℕ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) 2 *
    (HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) ((↑2 : ℂ) * -(I * (↑y : ℂ)))) =
  HPow.hPow (α := ℂ) (↑n : ℂ) (↑(-x) : ℂ) *
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))) 2
Tactic: rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ Summable (α := ℂ) fun (p : Nat.Primes) ↦
    -log
        (1 -
          HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑(↑p : ℕ) : ZMod N) : ℂ)
            (HPow.hPow (α := ℂ) (↑(↑p : ℕ) : ℂ) (-s)))
have this : ∀ (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 _)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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)))
have refine : (-s).re < -1
Tactic: refine (Nat.Primes.summable_rpow.mpr ?_).of_nonneg_of_le (fun _ ↦ norm_nonneg _) this
    |>.of_norm.clog_one_sub.neg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
⊢ ‖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 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
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (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 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
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + (↑x : ℂ)).re
h₁ : 1 < (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 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 (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
⊢ ‖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 H₀ : 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₀
-- 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 : ℂ)))))
⊢ ‖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 H₁ : 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₁
-- 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 : ℂ)))))
⊢ ‖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 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 : ℂ)))))
Tactic: have H₂ := summable_neg_log_one_sub_mul_prime_cpow (χ ^ 2) h₂
-- 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 : ℂ)))))
⊢ ‖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) ↦
  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