-- Mathlib/NumberTheory/LSeries/ZMod.lean
/--
The completed L-function of a function `ZMod N → ℂ` is differentiable, with the following
exceptions: at `s = 1` if `∑ j, Φ j ≠ 0`; and at `s = 0` if `Φ 0 ≠ 0`.
-/
lemma differentiableAt_completedLFunction (Φ : ZMod N → ℂ) (s : ℂ) (hs₀ : s ≠ 0 ∨ Φ 0 = 0)
    (hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0) : DifferentiableAt ℂ (completedLFunction Φ) s

Proof state:
case refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun x => ↑N ^ (-x) * ((∑ j : ZMod N, Φ j) / (1 - x))) s

Tactic:
refine .mul (by fun_prop) (hs₁.elim ?_ ?_)

Result:
case refine_2.refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ s ≠ 1 → DifferentiableAt ℂ (fun x => (∑ j : ZMod N, Φ j) / (1 - x)) s

case refine_2.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ ∑ j : ZMod N, Φ j = 0 → DifferentiableAt ℂ (fun x => (∑ j : ZMod N, Φ j) / (1 - x)) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
h : s ≠ 1
⊢ DifferentiableAt ℂ (fun x => ∑ j : ZMod N, Φ j) s

Tactic:
fun_prop

Result:
no goals

Proof state:
case refine_1.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ Φ 0 = 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

Tactic:
exact fun h ↦ by simp only [h, funext zero_div, differentiableAt_const]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ
    (fun x => completedLFunction₀ Φ x - ↑N ^ (-x) * (Φ 0 / x) - ↑N ^ (-x) * ((∑ j : ZMod N, Φ j) / (1 - x))) s

Tactic:
refine ((differentiable_completedLFunction₀ _ _).sub ?_).sub ?_

Result:
case refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun x => ↑N ^ (-x) * (Φ 0 / x)) s

case refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun x => ↑N ^ (-x) * ((∑ j : ZMod N, Φ j) / (1 - x))) s

Proof state:
case refine_2.refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ s ≠ 1 → DifferentiableAt ℂ (fun x => (∑ j : ZMod N, Φ j) / (1 - x)) s

Tactic:
exact fun h ↦ .div (by fun_prop) (by fun_prop) (by rwa [sub_ne_zero, ne_comm])

Result:
no goals

Proof state:
case refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun x => ↑N ^ (-x) * (Φ 0 / x)) s

Tactic:
refine .mul (by fun_prop) (hs₀.elim ?_ ?_)

Result:
case refine_1.refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ s ≠ 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

case refine_1.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ Φ 0 = 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

Proof state:
case refine_2.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ ∑ j : ZMod N, Φ j = 0 → DifferentiableAt ℂ (fun x => (∑ j : ZMod N, Φ j) / (1 - x)) s

Tactic:
exact fun h ↦ by simp only [h, zero_div, differentiableAt_const]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (completedLFunction Φ) s

Tactic:
simp only [funext (completedLFunction_eq Φ), mul_div_assoc]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ
    (fun x => completedLFunction₀ Φ x - ↑N ^ (-x) * (Φ 0 / x) - ↑N ^ (-x) * ((∑ j : ZMod N, Φ j) / (1 - x))) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
h : ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun x => (∑ j : ZMod N, Φ j) / (1 - x)) s

Tactic:
simp only [h, zero_div, differentiableAt_const]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun x => ↑N ^ (-x)) s

Tactic:
fun_prop

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
h : s ≠ 1
⊢ 1 - s ≠ 0

Tactic:
rwa [sub_ne_zero, ne_comm]

Result:
no goals

Proof state:
case refine_1.refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ s ≠ 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

Tactic:
exact fun h ↦ (differentiableAt_const _).div differentiableAt_id h

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
h : s ≠ 1
⊢ DifferentiableAt ℂ (HSub.hSub 1) s

Tactic:
fun_prop

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
h : Φ 0 = 0
⊢ DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

Tactic:
simp only [h, funext zero_div, differentiableAt_const]

Result:
no goals