-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
theorem completedLFunction_one_sub {χ : DirichletCharacter ℂ N} (hχ : IsPrimitive χ) (s : ℂ) :
    completedLFunction χ (1 - s) = N ^ (s - 1 / 2) * rootNumber χ * completedLFunction χ⁻¹ s

Proof state:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
let ε := I ^ (if χ.Even then 0 else 1)

Result:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (fun j => χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1))

Tactic:
rw [completedLFunction, completedLFunction_const_mul]

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) * χ (-1) / ε * (χ⁻¹ (-1) * gaussSum χ stdAddChar * ZMod.completedLFunction (⇑χ⁻¹) s) =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * ZMod.completedLFunction (⇑χ⁻¹) s * (χ (-1) * χ⁻¹ (-1))

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h : χ = 1
⊢ 1 = N

Tactic:
rwa [IsPrimitive, h, conductor_one (NeZero.ne _)] at hχ

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
⊢ ∑ j : ZMod N, χ j = 0

Tactic:
refine χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h : χ = 1
⊢ 1 = N

Proof state:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
have h_sum : ∑ j, χ j = 0 := by
  refine χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)
  rwa [IsPrimitive, h, conductor_one (NeZero.ne _)] at hχ

Result:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Proof state:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
rw [rootNumber, ← mul_comm_div, ← mul_comm_div, ← cpow_sub _ _ (NeZero.ne _), sub_sub, add_halves]

Result:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    (↑N ^ (s - 1) / I ^ if χ.Even then 0 else 1) * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 ⇑χ) s =
    ?m.72296 * ZMod.completedLFunction (fun j => χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s

Tactic:
congr 2 with j

Result:
case e_a.e_Φ.h
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
j : ZMod N
⊢ 𝓕 (⇑χ) j = χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j

Proof state:
case inl
s : ℂ
inst✝ : NeZero 1
χ : DirichletCharacter ℂ 1
hχ : χ.IsPrimitive
⊢ completedLFunction χ (1 - s) = ↑1 ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
simp [completedLFunction_modOne_eq, completedRiemannZeta_one_sub, rootNumber_modOne]

Result:
no goals

Proof state:
case neg
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Odd
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 1 * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun,
  pow_one, h, div_I, mul_neg_one, ← neg_mul, neg_neg]

Result:
no goals

Proof state:
case neg
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : ¬χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 1 * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
replace h : χ.Odd := χ.even_or_odd.resolve_left h

Result:
case neg
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Odd
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 1 * ZMod.completedLFunction (𝓕 ⇑χ) s

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
simp only [ε]

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    (↑N ^ (s - 1) * χ (-1) / I ^ if χ.Even then 0 else 1) * ZMod.completedLFunction (𝓕 ⇑χ) s

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1)) =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s

Tactic:
rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    (↑N ^ (s - 1) * χ (-1) / I ^ if χ.Even then 0 else 1) * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
split_ifs with h

Result:
case pos
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 0 * ZMod.completedLFunction (𝓕 ⇑χ) s

case neg
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : ¬χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 1 * ZMod.completedLFunction (𝓕 ⇑χ) s

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) * χ (-1) / ε * (χ⁻¹ (-1) * gaussSum χ stdAddChar * ZMod.completedLFunction (⇑χ⁻¹) s) =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * ZMod.completedLFunction (⇑χ⁻¹) s * (χ (-1) * χ⁻¹ (-1))

Tactic:
ring

Result:
no goals