-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
private lemma LFunction_ne_zero_of_not_quadratic_or_ne_one {t : ℝ} (h : χ ^ 2 ≠ 1 ∨ t ≠ 0) :
    LFunction χ (1 + I * t) ≠ 0

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
⊢ 4 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
⊢ False

Tactic:
have hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1 :=
  h.symm.imp_left <| mul_ne_zero two_ne_zero

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
⊢ False

Proof state:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
⊢ (1 / ↑0) ^ 3 * ↑0 ^ 4 * 1 = ↑0

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

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
⊢ False

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

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
⊢ False

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False

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

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
⊢ False

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h✝ : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
h : χ ^ 2 ≠ 1
H : χ = 1
⊢ False

Tactic:
simp only [H, one_pow, ne_eq, not_true_eq_false] at h

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
⊢ False

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₂

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
H :
  (fun x =>
      LFunctionTrivChar N (1 + ↑x) ^ 3 *
        (LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + I * ↑(2 * t)))) =O[𝓝[>] 0]
    fun x => (1 / ↑x) ^ 3 * (↑x ^ 4 * 1)
⊢ False

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
⊢ t ≠ 0 ∨ χ ≠ 1

Tactic:
refine h.symm.imp_right (fun h H ↦ ?_)

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h✝ : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
h : χ ^ 2 ≠ 1
H : χ = 1
⊢ False

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
H :
  (fun x =>
      LFunctionTrivChar N (1 + ↑x) ^ 3 *
        (LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + I * ↑(2 * t)))) =O[𝓝[>] 0]
    fun x => (1 / ↑x) ^ 3 * (↑x ^ 4 * 1)
⊢ False

Tactic:
simp only [ofReal_mul, ofReal_ofNat, mul_left_comm I, ← mul_assoc, help] at H

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
H :
  (fun x =>
      LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 *
        LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)) =O[𝓝[>] 0]
    fun x => ↑x
⊢ False

Proof state:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h✝ : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑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]

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
H :
  (fun x =>
      LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 *
        LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)) =O[𝓝[>] 0]
    fun x => ↑x
⊢ False

Tactic:
replace H := (H₀.trans H).norm_right

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
H : (fun x => 1) =O[𝓝[>] 0] fun x => ‖↑x‖
⊢ False

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
x : ℝ
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x

Tactic:
rcases eq_or_ne x 0 with rfl | h

Result:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
⊢ (1 / ↑0) ^ 3 * ↑0 ^ 4 * 1 = ↑0

case inr
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h✝ : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x