awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
⊢ t ≠ 0 ∨ χ ≠ 1

Tactic:
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
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
⊢ 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
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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 : ℂ)
inr : ∀ (h : x ≠ 0), HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)
⊢ HPow.hPow (β := ℕ) (1 / (↑x : ℂ)) 3 * HPow.hPow (β := ℕ) (↑x : ℂ) 4 * 1 = (↑x : ℂ)

Tactic:
rcases eq_or_ne x 0 with rfl | h

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
⊢ Ne (α := ℕ) 4 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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
inl₃ inl₄ : Eq (α := ℂ) 0 0
⊢ HPow.hPow (β := ℕ) (1 / (↑0 : ℂ)) 3 * HPow.hPow (β := ℕ) (↑0 : ℂ) 4 * 1 = (↑0 : ℂ)

Tactic:
rw [ofReal_zero, zero_pow (by lia), mul_zero, mul_one]

Premises used: MulZeroClass.mul_zero, Complex.ofReal_zero, mul_one, zero_pow
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h_1 : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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 : ℂ)
inr₆ inr₇ : (↑x : ℂ) = (↑x : ℂ)
⊢ HPow.hPow (β := ℕ) (1 / (↑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]

Premises used: Iff.mpr, pow_succ, mul_assoc, Complex.ofReal_ne_zero, pow_ne_zero, inv_pow, one_div, mul_one, OfNat.ofNat, inv_mul_cancel₀, one_mul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ HPow.hPow (β := ℕ) χ 2 ≠ 1
⊢ ∀ (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]
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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 : ℂ)
⊢ 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
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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 : ℂ))
⊢ 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₂
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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)
⊢ 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

Premises used: mul_assoc, mul_left_comm, Complex.ofReal_ofNat, Complex.ofReal_mul, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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 : ℂ)
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ ‖(↑x : ℂ)‖

Tactic:
replace H := (H₀.trans H).norm_right
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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 : ℂ)‖
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ ‖x‖

Tactic:
simp only [norm_real] at H

Premises used: Complex.norm_real
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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

Tactic:
isLittleO_irrefl (.of_forall (fun _ ↦ one_ne_zero)) <|
    H.of_norm_right.trans_isLittleO <| isLittleO_id_one.mono nhdsWithin_le_nhds

Premises used: Filter.Frequently.of_forall, Asymptotics.isLittleO_irrefl, Asymptotics.isLittleO_id_one, nhdsWithin_le_nhds, Asymptotics.IsBigO.of_norm_right, Asymptotics.IsBigO.trans_isLittleO, one_ne_zero, Asymptotics.IsLittleO.mono
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
t : ℝ
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * (↑t : ℂ)) = 0
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

Tactic:
exact isLittleO_irrefl (.of_forall (fun _ ↦ one_ne_zero)) <|
    H.of_norm_right.trans_isLittleO <| isLittleO_id_one.mono nhdsWithin_le_nhds

Premises used: Filter.Frequently.of_forall, Asymptotics.isLittleO_irrefl, Asymptotics.isLittleO_id_one, nhdsWithin_le_nhds, Asymptotics.IsBigO.of_norm_right, Asymptotics.IsBigO.trans_isLittleO, one_ne_zero, Asymptotics.IsLittleO.mono
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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
neg : ∀ (h : ¬(HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1)), LFunction χ s ≠ 0
⊢ LFunction χ s ≠ 0

Tactic:
by_cases h : χ ^ 2 = 1 ∧ s = 1
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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

Tactic:
exact h.2 ▸ LFunction_apply_one_ne_zero_of_quadratic h.1 <| hχs.neg_resolve_right h.2

Premises used: Or.neg_resolve_right, And.right
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(HPow.hPow (β := ℕ) χ 2 = 1 ∧ s = 1)
rw : 1 + I * (↑s.im : ℂ)
| s

Tactic:
rw [← re_add_im s, hs, ofReal_one, mul_comm]

Premises used: Complex.ofReal_one, mul_comm, Complex.re_add_im
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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 : ℂ)
conv_lhs₁ : 1 + I * (↑s.im : ℂ) = 1 + I * (↑s.im : ℂ)
⊢ s = 1 + I * (↑s.im : ℂ)

Tactic:
conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]

Premises used: Complex.ofReal_one, mul_comm, Complex.re_add_im
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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 : ℂ)

Tactic:
have hs' : s = 1 + I * s.im := by
      conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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 : ℂ)
⊢ HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ I * (↑s.im : ℂ) ≠ 0

Tactic:
rw [not_and_or, ← ne_eq, ← ne_eq, hs', add_ne_left] at h

Premises used: ne_eq, add_ne_left, not_and_or
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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 : ℂ)
h₁ : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ I * (↑s.im : ℂ) ≠ 0
⊢ s = 1 + I * (↑s.im : ℂ)

Tactic:
rw [not_and_or, ← ne_eq, ← ne_eq, hs', add_ne_left] at h

Premises used: ne_eq, add_ne_left, not_and_or
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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 : ℂ)
H : I * (↑s.im : ℂ) ≠ 0
⊢ s.im ≠ 0

Tactic:
exact_mod_cast right_ne_zero_of_mul H

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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 : ℂ)
⊢ 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)
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
hs' : s = 1 + I * (↑s.im : ℂ)
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ s.im ≠ 0
⊢ LFunction χ s ≠ 0

Tactic:
hs'.symm ▸ χ.LFunction_ne_zero_of_not_quadratic_or_ne_one h

Premises used: Eq.rec, _private.0.DirichletCharacter.LFunction_ne_zero_of_not_quadratic_or_ne_one, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
hs' : s = 1 + I * (↑s.im : ℂ)
h : HPow.hPow (β := ℕ) χ 2 ≠ 1 ∨ s.im ≠ 0
⊢ LFunction χ s ≠ 0

Tactic:
exact hs'.symm ▸ χ.LFunction_ne_zero_of_not_quadratic_or_ne_one h
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
s : ℂ
hχs : χ ≠ 1 ∨ s ≠ 1
hs : 1 ≤ s.re
⊢ LFunction χ s ≠ 0

Tactic:
hs.eq_or_lt.casesOn (fun hs ↦ LFunction_ne_zero_of_re_eq_one χ hs.symm hχs)
    fun hs ↦ LFunction_eq_LSeries χ hs ▸ LSeries_ne_zero_of_one_lt_re χ hs

Premises used: LE.le.eq_or_lt, Or.casesOn
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
inst : NeZero N
hχ : χ ≠ 1
⊢ LFunction χ 1 ≠ 0

Tactic:
LFunction_ne_zero_of_one_le_re χ (.inl hχ) <| one_re ▸ le_rfl

Premises used: le_rfl, Eq.rec, DirichletCharacter.LFunction_ne_zero_of_one_le_re, Or.inl, Complex.one_re
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
s : ℂ
hs : 1 ≤ s.re
inl : ∀ (hs : 1 ≤ re 1), riemannZeta 1 ≠ 0
inr : ∀ (hs₀ : s ≠ 1), riemannZeta s ≠ 0
⊢ riemannZeta s ≠ 0

Tactic:
rcases eq_or_ne s 1 with rfl | hs₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
hs : 1 ≤ re 1
⊢ riemannZeta 1 ≠ 0

Tactic:
riemannZeta_one_ne_zero

Premises used: riemannZeta_one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
hs : 1 ≤ re 1
⊢ riemannZeta 1 ≠ 0

Tactic:
exact riemannZeta_one_ne_zero

Premises used: riemannZeta_one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
s : ℂ
hs : 1 ≤ s.re
hs₀ : s ≠ 1
⊢ riemannZeta s ≠ 0

Tactic:
LFunction_modOne_eq (χ := 1) ▸ LFunction_ne_zero_of_one_le_re _ (.inr hs₀) hs

Premises used: DirichletCharacter.LFunction_modOne_eq, Eq.rec, DirichletCharacter.LFunction_ne_zero_of_one_le_re, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
s : ℂ
hs : 1 ≤ s.re
hs₀ : s ≠ 1
⊢ riemannZeta s ≠ 0

Tactic:
exact LFunction_modOne_eq (χ := 1) ▸ LFunction_ne_zero_of_one_le_re _ (.inr hs₀) hs
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n : ℕ
rw : LE.le (α := ℂ) 0 (∑' (n_1 : ℕ), term (logMul^[n] a) (↑x : ℂ) n_1)
⊢ 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n (LSeries a) (↑x : ℂ)

Tactic:
rw [LSeries_iteratedDeriv _ h, LSeries, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨n, rfl⟩,
    one_mul]

Premises used: LSeries_iteratedDeriv, mul_assoc, pow_add, Even.neg_one_pow, LSeries, Exists.intro, one_mul, rfl
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n : ℕ
⊢ LE.le (α := ℂ) 0 (∑' (n_1 : ℕ), term (logMul^[n] a) (↑x : ℂ) n_1)

Tactic:
tsum_nonneg fun k ↦ ?_

Premises used: tsum_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n : ℕ
refine : ∀ (k : ℕ), 0 ≤ term (logMul^[n] a) (↑x : ℂ) k
⊢ LE.le (α := ℂ) 0 (∑' (n_1 : ℕ), term (logMul^[n] a) (↑x : ℂ) n_1)

Tactic:
refine tsum_nonneg fun k ↦ ?_

Premises used: tsum_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
isTrue : k = 0 → LE.le (α := ℂ) 0 0
isFalse : ¬k = 0 → 0 ≤ logMul^[n] a k / HPow.hPow (α := ℂ) (↑k : ℂ) (↑x : ℂ)
⊢ 0 ≤ if k = 0 then 0 else logMul^[n] a k / HPow.hPow (α := ℂ) (↑k : ℂ) (↑x : ℂ)

Tactic:
split
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
h_1 : k = 0
⊢ LE.le (α := ℂ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
h_1 : k = 0
⊢ LE.le (α := ℂ) 0 0

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
h_1 : ¬k = 0
⊢ k ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
h_1 : ¬k = 0
isFalse : 0 ≤ logMul^[n] a k
⊢ 0 ≤ logMul^[n] a k / HPow.hPow (α := ℂ) (↑k : ℂ) (↑x : ℂ)

Tactic:
refine mul_nonneg ?_ <| (inv_natCast_cpow_ofReal_pos (by assumption) x).le

Premises used: mul_nonneg, LT.lt.le, Complex.inv_natCast_cpow_ofReal_pos
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
k : ℕ
h_1 : ¬k = 0
⊢ 0 ≤ logMul^[0] a k

Tactic:
simpa only [Function.iterate_zero, id_eq] using hn k

Premises used: Function.iterate_zero, id_eq
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
k : ℕ
h_1 : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
isFalse : 0 ≤ logMul (logMul^[n] a) k
⊢ 0 ≤ logMul^[n + 1] a k

Tactic:
rw [Function.iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.NumberTheory.LSeries.Positivity
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

Tactic:
mul_nonneg ?_ IH

Premises used: mul_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
k : ℕ
h_1 : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
isFalse : 0 ≤ log (↑k : ℂ)
⊢ 0 ≤ logMul (logMul^[n] a) k

Tactic:
refine mul_nonneg ?_ IH

Premises used: mul_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
k : ℕ
h_1 : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ log (↑k : ℂ)

Tactic:
simp only [← natCast_log, zero_le_real, Real.log_natCast_nonneg]

Premises used: Complex.natCast_log, Real.log_natCast_nonneg, Complex.zero_le_real
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < (↑x : EReal)
n k : ℕ
h_1 : ¬k = 0
isFalse : 0 ≤ logMul^[0] a k
isFalse₁ : ∀ (n : ℕ) (IH : 0 ≤ logMul^[n] a k), 0 ≤ logMul^[n + 1] a k
⊢ 0 ≤ logMul^[n] 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]

Premises used: Function.iterate_succ_apply', Function.iterate_zero, Complex.natCast_log, Real.log_natCast_nonneg, Complex.zero_le_real, id_eq
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < (↑x : EReal)
⊢ LT.lt (α := ℂ) 0 (∑' (n : ℕ), term a (↑x : ℂ) n)

Tactic:
Summable.tsum_pos ?_ (fun n ↦ term_nonneg (ha₀ n) x) 1 <| term_pos one_ne_zero ha₁ x

Premises used: Summable.tsum_pos, LSeries.term_nonneg, LSeries.term_pos, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < (↑x : EReal)
refine : Summable (term a (↑x : ℂ))
⊢ LT.lt (α := ℂ) 0 (∑' (n : ℕ), term a (↑x : ℂ) n)

Tactic:
refine Summable.tsum_pos ?_ (fun n ↦ term_nonneg (ha₀ n) x) 1 <| term_pos one_ne_zero ha₁ x

Premises used: Summable.tsum_pos, LSeries.term_nonneg, LSeries.term_pos, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < (↑x : EReal)
⊢ abscissaOfAbsConv a < (↑(↑x : ℂ).re : EReal)

Tactic:
simpa only [ofReal_re] using hx

Premises used: Complex.ofReal_re
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < (↑x : EReal)
⊢ Summable (term a (↑x : ℂ))

Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simpa only [ofReal_re] using hx

Premises used: LSeriesSummable_of_abscissaOfAbsConv_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Positivity
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 : ℝ
⊢ x < max x y + 1

Tactic:
have hxy : x < max x y + 1 := (le_max_left x y).trans_lt (lt_add_one _)
-- Module: Mathlib.NumberTheory.LSeries.Positivity
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
⊢ abscissaOfAbsConv a < (↑(max x y) : EReal) + 1

Tactic:
have hxy' : abscissaOfAbsConv a < max x y + 1 := hx.trans_lt <| mod_cast hxy