awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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 ≤
    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))
have 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
Tactic: convert! (show 0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 by positivity) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
⊢ 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
have 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
Tactic: by_cases hn' : IsUnit (n : ZMod N)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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
⊢ 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
have 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
Tactic: by_cases hn' : IsUnit (n : ZMod N)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
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
have rw : HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ 0 ∨ 1 < HPow.hPow (α := ℝ) (↑n : ℝ) x
Tactic: rw [Real.rpow_neg (Nat.cast_nonneg n), inv_lt_one_iff₀]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
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
have hn₁ : 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
-- 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
⊢ ‖HMul.hMul (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑n : ZMod N) : ℂ) (HPow.hPow (α := ℂ) (↑n : ℂ) (-(I * (↑y : ℂ))))‖ = 1
have rw : 1 * HPow.hPow (α := ℝ) (↑n : ℝ) (-(I * (↑y : ℂ))).re = 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
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 ≤
    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
have hz : ‖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]
-- 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
⊢ 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
have 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
Tactic: rw [MulChar.one_apply hn', one_mul]
-- 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
⊢ 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
have h : log (1 - HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ))) = log (1 - (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ))
Tactic: convert! re_log_comb_nonneg' (by positivity) hn hz using 6
-- 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 : log (1 - HPow.hPow (α := ℂ) (↑n : ℂ) (-(↑x : ℂ))) = log (1 - (↑(HPow.hPow (α := ℝ) (↑n : ℝ) (-x)) : ℂ))
⊢ 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
have 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 : ℂ)))))
Tactic: convert! re_log_comb_nonneg' (by positivity) hn hz using 6
-- 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 : 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 : ℂ)))))
⊢ 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
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: convert! re_log_comb_nonneg' (by positivity) hn hz using 6
-- 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
⊢ 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 : ℂ)))))
have 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 : ℂ))))
Tactic: congr 2
-- 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
⊢ 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 : 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]
-- 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 : ℂ))))
⊢ 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₁ : 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 : ℂ))))
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
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 : ℂ))))
⊢ 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₂ : 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 : ℂ))))
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
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 : ℂ))))
⊢ 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₃ : 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 : ℂ))))
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
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 : ℂ))))
⊢ 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₄ : 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 : ℂ))))
Tactic: rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, mul_left_comm]