-- Mathlib/NumberTheory/LSeries/ZMod.lean
theorem completedLFunction_one_sub_odd (hΦ : Φ.Odd) (s : ℂ) :
    completedLFunction Φ (1 - s) = N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
have hF : Differentiable ℂ F := (differentiable_completedLFunction hΦ.map_zero
  hΦ.sum_eq_zero).comp (differentiable_id.const_sub 1)

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
this : {z | 1 < z.re} ∈ 𝓝 2
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
have hFG : F =ᶠ[𝓝 2] G := by filter_upwards [this] with t ht
  using completedLFunction_one_sub_of_one_lt_odd hΦ ht

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
this : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
⊢ Differentiable ℂ (completedLFunction (𝓕 Φ))

Tactic:
rw [← dft_odd_iff] at hΦ

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd (𝓕 Φ)
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
⊢ Differentiable ℂ (completedLFunction (𝓕 Φ))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
this : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
rw [← analyticOnNhd_univ_iff_differentiable] at hF hG

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : AnalyticOnNhd ℂ F Set.univ
hG : AnalyticOnNhd ℂ G Set.univ
this : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd (𝓕 Φ)
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
⊢ Differentiable ℂ (completedLFunction (𝓕 Φ))

Tactic:
exact differentiable_completedLFunction hΦ.map_zero hΦ.sum_eq_zero

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
have hG : Differentiable ℂ G := by
  apply (((differentiable_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul_const _).mul
  rw [← dft_odd_iff] at hΦ
  exact differentiable_completedLFunction hΦ.map_zero hΦ.sum_eq_zero

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
let G (t) := ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
let F (t) := completedLFunction Φ (1 - t)

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : AnalyticOnNhd ℂ F Set.univ
hG : AnalyticOnNhd ℂ G Set.univ
this : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
exact congr_fun (hF.eq_of_eventuallyEq hG hFG) s

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
⊢ Differentiable ℂ G

Tactic:
apply (((differentiable_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul_const _).mul

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
⊢ Differentiable ℂ (completedLFunction (𝓕 Φ))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
this : {z | 1 < z.re} ∈ 𝓝 2
⊢ F =ᶠ[𝓝 2] G

Tactic:
filter_upwards [this] with t ht
using completedLFunction_one_sub_of_one_lt_odd hΦ ht

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
⊢ 2 ∈ re ⁻¹' Set.Ioi 1

Tactic:
simp

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
have : {z | 1 < re z} ∈ 𝓝 2 := (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp)

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t => completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t => ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
this : {z | 1 < z.re} ∈ 𝓝 2
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s