-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
lemma zetaMul_prime_pow_nonneg {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) {p : ℕ}
    (hp : p.Prime) (k : ℕ) :
    0 ≤ zetaMul χ (p ^ k)

Proof state:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = 0
⊢ 0 ≤ ∑ x ∈ Finset.range (k + 1), χ ↑p ^ x

Tactic:
refine Finset.sum_nonneg fun i _ ↦ ?_

Result:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = 0
i : ℕ
x✝ : i ∈ Finset.range (k + 1)
⊢ 0 ≤ χ ↑p ^ i

Proof state:
case inr.inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = 1
i : ℕ
x✝ : i ∈ Finset.range (k + 1)
⊢ 0 ≤ χ ↑p ^ i

Tactic:
simp only [h, one_pow, zero_le_one]

Result:
no goals

Proof state:
case inr.inr
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = -1
⊢ 0 ≤ if _root_.Even (k + 1) then 0 else 1

Tactic:
split_ifs

Result:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = -1
h✝ : _root_.Even (k + 1)
⊢ 0 ≤ 0

case neg
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = -1
h✝ : ¬_root_.Even (k + 1)
⊢ 0 ≤ 1

Proof state:
case inr.inr
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = -1
⊢ 0 ≤ ∑ x ∈ Finset.range (k + 1), χ ↑p ^ x

Tactic:
simp only [h, neg_one_geom_sum]

Result:
case inr.inr
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = -1
⊢ 0 ≤ if _root_.Even (k + 1) then 0 else 1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
⊢ 0 ≤ χ.zetaMul (p ^ k)

Tactic:
simp only [zetaMul, toArithmeticFunction, coe_zeta_mul_apply, coe_mk,
  Nat.sum_divisors_prime_pow hp, pow_eq_zero_iff', hp.ne_zero, ne_eq, false_and, ↓reduceIte,
  Nat.cast_pow, map_pow]

Result:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
⊢ 0 ≤ ∑ x ∈ Finset.range (k + 1), χ ↑p ^ x

Proof state:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = 0
i : ℕ
x✝ : i ∈ Finset.range (k + 1)
⊢ 0 ≤ χ ↑p ^ i

Tactic:
simp only [h, le_refl, pow_nonneg]

Result:
no goals

Proof state:
case inr.inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = 1
⊢ 0 ≤ ∑ x ∈ Finset.range (k + 1), χ ↑p ^ x

Tactic:
refine Finset.sum_nonneg fun i _ ↦ ?_

Result:
case inr.inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = 1
i : ℕ
x✝ : i ∈ Finset.range (k + 1)
⊢ 0 ≤ χ ↑p ^ i

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
⊢ 0 ≤ ∑ x ∈ Finset.range (k + 1), χ ↑p ^ x

Tactic:
rcases MulChar.isQuadratic_iff_sq_eq_one.mpr hχ p with h | h | h

Result:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = 0
⊢ 0 ≤ ∑ x ∈ Finset.range (k + 1), χ ↑p ^ x

case inr.inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = 1
⊢ 0 ≤ ∑ x ∈ Finset.range (k + 1), χ ↑p ^ x

case inr.inr
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = -1
⊢ 0 ≤ ∑ x ∈ Finset.range (k + 1), χ ↑p ^ x

Proof state:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = -1
h✝ : _root_.Even (k + 1)
⊢ 0 ≤ 0

case neg
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = -1
h✝ : ¬_root_.Even (k + 1)
⊢ 0 ≤ 1

Tactic:
exacts [le_rfl, zero_le_one]

Result:
no goals