awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℂ)
inr₄ : 1 * (↑x : ℂ) * 1 = (↑x : ℂ)
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
have inr₅ : (↑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 : ℂ)
inr₄ : 1 * (↑x : ℂ) * 1 = (↑x : ℂ)
inr₅ : (↑x : ℂ) * 1 = (↑x : ℂ)
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
have inr₆ : (↑x : ℂ) = (↑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 (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
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
⊢ False
have help : ∀ (x : ℝ), HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
Tactic: have help (x : ℝ) : ((1 / x) ^ 3 * x ^ 4 * 1 : ℂ) = x := by
    rcases eq_or_ne x 0 with rfl | h
    · rw [ofReal_zero, zero_pow (by lia), mul_zero, mul_one]
    · 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 (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
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
help : ∀ (x : ℝ), HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
⊢ False
have H₀ : IsBigO (E := ℝ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦
  HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
      HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑t : ℂ))) 4 *
    LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + 2 * I * (↑t : ℂ))
Tactic: have H₀ : (fun _ : ℝ ↦ (1 : ℝ)) =O[𝓝[>] 0]
      fun x ↦ LFunctionTrivChar N (1 + x) ^ 3 * LFunction χ (1 + x + I * t) ^ 4 *
                   LFunction (χ ^ 2) (1 + x + 2 * I * t) :=
    IsBigO.of_bound' <| eventually_nhdsWithin_of_forall
      fun _ hx ↦ (norm_one (α := ℝ)).symm ▸ (χ.norm_LFunction_product_ge_one hx t).le
-- 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
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
help : ∀ (x : ℝ), HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
H₀ :
  IsBigO (E := ℝ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
        HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑t : ℂ))) 4 *
      LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + 2 * I * (↑t : ℂ))
⊢ False
have H : IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0)
  (fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
      (HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑t : ℂ))) 4 *
        LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + I * (↑(2 * t) : ℂ))))
  fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * (HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1)
Tactic: have H := (LFunctionTrivChar_isBigO_near_one_horizontal (N := N)).pow 3 |>.mul <|
    (χ.LFunction_isBigO_horizontal_of_eq_zero hz₁ Hz).pow 4 |>.mul <|
    LFunction_isBigO_horizontal _ hz₂
-- 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
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
help : ∀ (x : ℝ), HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
H₀ :
  IsBigO (E := ℝ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
        HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑t : ℂ))) 4 *
      LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + 2 * I * (↑t : ℂ))
H :
  IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
        (HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑t : ℂ))) 4 *
          LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + I * (↑(2 * t) : ℂ))))
    fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * (HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1)
⊢ False
have H₁ : IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0)
  (fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
        HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑t : ℂ))) 4 *
      LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + 2 * I * (↑t : ℂ)))
  fun (x : ℝ) ↦ (↑x : ℂ)
Tactic: simp only [ofReal_mul, ofReal_ofNat, mul_left_comm I, ← mul_assoc, help] at H
Cleared hypotheses: 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
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
help : ∀ (x : ℝ), HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
H₀ :
  IsBigO (E := ℝ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
        HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑t : ℂ))) 4 *
      LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + 2 * I * (↑t : ℂ))
H :
  IsBigO (E := ℂ) (F := ℂ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
          HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑t : ℂ))) 4 *
        LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + 2 * I * (↑t : ℂ)))
    fun (x : ℝ) ↦ (↑x : ℂ)
⊢ False
have H₁ : IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ ‖(↑x : ℂ)‖
Tactic: replace H := (H₀.trans H).norm_right
Cleared hypotheses: 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
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
help : ∀ (x : ℝ), HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
H₀ :
  IsBigO (E := ℝ) (F := ℂ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) (LFunctionTrivChar N (1 + (↑x : ℂ))) 3 *
        HPow.hPow (β := ℕ) (LFunction χ (1 + (↑x : ℂ) + I * (↑t : ℂ))) 4 *
      LFunction (HPow.hPow (β := ℕ) χ 2) (1 + (↑x : ℂ) + 2 * I * (↑t : ℂ))
H : IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ ‖(↑x : ℂ)‖
⊢ False
have H₁ : IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ ‖x‖
Tactic: simp only [norm_real] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
⊢ LFunction χ s ≠ 0
have pos : ∀ (h : HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1), LFunction χ s ≠ 0
Tactic: by_cases h : χ ^ 2 = 1 ∧ s = 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
pos : ∀ (h : HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1), LFunction χ s ≠ 0
⊢ LFunction χ s ≠ 0
have neg : ∀ (h : ¬(HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1)), LFunction χ s ≠ 0
Tactic: by_cases h : χ ^ 2 = 1 ∧ s = 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1)
| s
have rw : 1 + I * (↑s.im : ℂ)
Tactic: rw [← re_add_im s, hs, ofReal_one, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1)
⊢ s = 1 + I * (↑s.im : ℂ)
have conv_lhs : s = 1 + I * (↑s.im : ℂ)
Tactic: conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1)
conv_lhs : s = 1 + I * (↑s.im : ℂ)
⊢ s = 1 + I * (↑s.im : ℂ)
have conv_lhs₁ : 1 + I * (↑s.im : ℂ) = 1 + I * (↑s.im : ℂ)
Tactic: conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1)
⊢ LFunction χ s ≠ 0
have hs' : s = 1 + I * (↑s.im : ℂ)
Tactic: have hs' : s = 1 + I * s.im := by
      conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1)
hs' : s = 1 + I * (↑s.im : ℂ)
⊢ LFunction χ s ≠ 0
have h₁ : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ I * (↑s.im : ℂ) ≠ 0
Tactic: rw [not_and_or, ← ne_eq, ← ne_eq, hs', add_ne_left] at h
Cleared hypotheses: h, hs'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (hypothesis)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ I * (↑s.im : ℂ) ≠ 0
hs' : s = 1 + I * (↑s.im : ℂ)
⊢ LFunction χ s ≠ 0
have h₁ : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ s.im ≠ 0
Tactic: replace h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0 :=
      h.imp_right (fun H ↦ by exact_mod_cast right_ne_zero_of_mul H)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
s : ℂ
hs : 1 ≤ s.re
⊢ riemannZeta s ≠ 0
have inl : ∀ (hs : 1 ≤ re 1), riemannZeta 1 ≠ 0
Tactic: rcases eq_or_ne s 1 with rfl | hs₀
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
s : ℂ
hs : 1 ≤ s.re
inl : ∀ (hs : 1 ≤ re 1), riemannZeta 1 ≠ 0
⊢ riemannZeta s ≠ 0
have inr : ∀ (hs₀ : s ≠ 1), riemannZeta s ≠ 0
Tactic: rcases eq_or_ne s 1 with rfl | hs₀
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n : ℕ
⊢ 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n (LSeries a) (↑x : ℂ)
have rw : LE.le (α := ℂ) 0 (∑' (n_1 : ℕ), term (logMul^[n] a) (↑x : ℂ) n_1)
Tactic: rw [LSeries_iteratedDeriv _ h, LSeries, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨n, rfl⟩,
    one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n : ℕ
⊢ LE.le (α := ℂ) 0 (∑' (n_1 : ℕ), term (logMul^[n] a) (↑x : ℂ) n_1)
have refine : ∀ (k : ℕ), 0 ≤ term (logMul^[n] a) (↑x : ℂ) k
Tactic: refine tsum_nonneg fun k ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
⊢ 0 ≤ if k = 0 then 0 else logMul^[n] a k / HPow.hPow (α := ℂ) (↑k : ℂ) (↑x : ℂ)
have isTrue : k = 0 → LE.le (α := ℂ) 0 0
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
isTrue : k = 0 → LE.le (α := ℂ) 0 0
⊢ 0 ≤ if k = 0 then 0 else logMul^[n] a k / HPow.hPow (α := ℂ) (↑k : ℂ) (↑x : ℂ)
have isFalse : ¬k = 0 → 0 ≤ logMul^[n] a k / HPow.hPow (α := ℂ) (↑k : ℂ) (↑x : ℂ)
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
h_1 : ¬k = 0
⊢ 0 ≤ logMul^[n] a k / HPow.hPow (α := ℂ) (↑k : ℂ) (↑x : ℂ)
have isFalse : 0 ≤ logMul^[n] a k
Tactic: refine mul_nonneg ?_ <| (inv_natCast_cpow_ofReal_pos (by assumption) x).le
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
k : ℕ
h_1 : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ logMul^[n + 1] a k
have isFalse : 0 ≤ logMul (logMul^[n] a) k
Tactic: rw [Function.iterate_succ_apply']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
k : ℕ
h_1 : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ logMul (logMul^[n] a) k
have isFalse : 0 ≤ log (↑k : ℂ)
Tactic: refine mul_nonneg ?_ IH
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
h_1 : ¬k = 0
⊢ 0 ≤ logMul^[n] a k
have isFalse : 0 ≤ logMul^[0] a k
Tactic: induction n with
    | zero => simpa only [Function.iterate_zero, id_eq] using hn k
    | succ n IH =>
        rw [Function.iterate_succ_apply']
        refine mul_nonneg ?_ IH
        simp only [← natCast_log, zero_le_real, Real.log_natCast_nonneg]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
h_1 : ¬k = 0
isFalse : 0 ≤ logMul^[0] a k
⊢ 0 ≤ logMul^[n] a k
have isFalse₁ : ∀ (n : ℕ) (IH : 0 ≤ logMul^[n] a k), 0 ≤ logMul^[n + 1] a k
Tactic: induction n with
    | zero => simpa only [Function.iterate_zero, id_eq] using hn k
    | succ n IH =>
        rw [Function.iterate_succ_apply']
        refine mul_nonneg ?_ IH
        simp only [← natCast_log, zero_le_real, Real.log_natCast_nonneg]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < (↑x : EReal)
⊢ LT.lt (α := ℂ) 0 (∑' (n : ℕ), term a (↑x : ℂ) n)
have refine : Summable (term a (↑x : ℂ))
Tactic: refine Summable.tsum_pos ?_ (fun n ↦ term_nonneg (ha₀ n) x) 1 <| term_pos one_ne_zero ha₁ x
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (hypothesis)
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
⊢ 0 < f (↑y : ℂ)
have hxy : x < max x y + 1
Tactic: have hxy : x < max x y + 1 := (le_max_left x y).trans_lt (lt_add_one _)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (hypothesis)
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
⊢ 0 < f (↑y : ℂ)
have hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
Tactic: have hxy' : abscissaOfAbsConv a < max x y + 1 := hx.trans_lt <| mod_cast hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (hypothesis)
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
⊢ 0 < f (↑y : ℂ)
have hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
Tactic: have hys : (max x y + 1 : ℂ) ∈ {s | x < s.re} := by
    simp only [Set.mem_setOf_eq, add_re, ofReal_re, one_re, hxy]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (hypothesis)
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
⊢ 0 < f (↑y : ℂ)
have hfx : 0 < f ((↑(max x y) : ℂ) + 1)
Tactic: have hfx : 0 < f (max x y + 1) := by
    simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
hfx : 0 < f ((↑(max x y) : ℂ) + 1)
⊢ 0 < f (↑y : ℂ)
have refine_1 : ∀ (n : ℕ), n ≠ 0 → 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f ((↑(max x y) : ℂ) + 1)
Tactic: refine (hfx.trans_le <| hf.apply_le_of_iteratedDeriv_alternating (fun n _ ↦ ?_) ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (goal)
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
hfx : 0 < f ((↑(max x y) : ℂ) + 1)
refine_1 : ∀ (n : ℕ), n ≠ 0 → 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f ((↑(max x y) : ℂ) + 1)
⊢ 0 < f (↑y : ℂ)
have refine_2 : (↑y : ℂ) ≤ (↑(max x y) : ℂ) + 1
Tactic: refine (hfx.trans_le <| hf.apply_le_of_iteratedDeriv_alternating (fun n _ ↦ ?_) ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Positivity (hypothesis)
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
hfx : 0 < f ((↑(max x y) : ℂ) + 1)
n : ℕ
h : n ≠ 0
⊢ 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f ((↑(max x y) : ℂ) + 1)
have hs : IsOpen (X := ℂ) {s : ℂ | x < s.re}
Tactic: have hs : IsOpen {s : ℂ | x < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
⊢ Eq.{u_1 + 1} (α := α) (∏' (n : ℕ), f n) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1)))
have hfm' : Multipliable.{u_1, 0} (α := α) fun (pk : Nat.Primes × ℕ) ↦ f ((↑pk.1 : ℕ) ^ (pk.2 + 1))
Tactic: have hfm' : Multipliable fun pk : Nat.Primes × ℕ ↦ f (pk.fst ^ (pk.snd + 1)) :=
    prodNatEquiv.symm.multipliable_iff.mp <| by
      simpa only [← coe_prodNatEquiv_apply, Prod.eta, Function.comp_def, Equiv.apply_symm_apply]
        using hfm.subtype _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfm' : Multipliable.{u_1, 0} (α := α) fun (pk : Nat.Primes × ℕ) ↦ f ((↑pk.1 : ℕ) ^ (pk.2 + 1))
⊢ Eq.{u_1 + 1} (α := α) (∏' (n : ℕ), f n) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1)))
have simp : Eq.{u_1 + 1} (α := α)
  (∏' (c : Nat.Primes × ℕ), f (↑((prodNatEquiv : (a : Nat.Primes × ℕ) → { n : ℕ // IsPrimePow n }) c) : ℕ))
  (∏' (p : Nat.Primes × ℕ), f ((↑p.1 : ℕ) ^ (p.2 + 1)))
Tactic: simp only [← tprod_subtype_eq_of_mulSupport_subset hf, Set.coe_setOf, ← prodNatEquiv.tprod_eq,
    ← hfm'.tprod_prod]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
⊢ ∏' (n : ℕ), f n =
    HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))
have rw : ∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1)) =
  HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))
Tactic: rw [tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers hfm hf]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
⊢ ∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1)) =
    HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))
have hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
Tactic: have hfs' (p : Nat.Primes) : Multipliable fun k : ℕ ↦ f (p ^ (k + 1)) :=
    hfm.comp_injective <| (strictMono_nat_of_lt_succ
      fun k ↦ pow_lt_pow_right₀ p.prop.one_lt <| lt_add_one (k + 1)).injective
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
| ∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1))
have h : ∀ (p : Nat.Primes), ∏' (k : ℕ), f ((↑p : ℕ) ^ (k + 1))
Tactic: enter [1, p]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
p : Nat.Primes
| ∏' (k : ℕ), f ((↑p : ℕ) ^ (k + 1))
have h : f (↑p : ℕ) * ∏' (b : ℕ), f ((↑p : ℕ) ^ (b + 1 + 1))
Tactic: rw [(hfs' p).tprod_eq_zero_mul, zero_add, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
p : Nat.Primes
| f (↑p : ℕ) * ∏' (b : ℕ), f ((↑p : ℕ) ^ (b + 1 + 1))
have h : ∀ (k : ℕ), f ((↑p : ℕ) ^ (k + 1 + 1))
Tactic: enter [2, 1, k]