-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The auxiliary function is continuous away from the zeros of the L-functions of the Dirichlet
characters mod `q` (including at `s = 1`). -/
lemma continuousOn_LFunctionResidueClassAux' :
    ContinuousOn (LFunctionResidueClassAux a)
      {s | s = 1 ∨ ∀ χ : DirichletCharacter ℂ q, LFunction χ s ≠ 0}

Proof state:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s => ∑ x ∈ {1}ᶜ, x a⁻¹ * (-deriv (LFunction x) s / LFunction x s))
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
refine continuousOn_finset_sum _ fun χ hχ ↦ continuousOn_const.mul ?_

Result:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ∈ {1}ᶜ
⊢ ContinuousOn (fun s => -deriv (LFunction χ) s / LFunction χ s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Proof state:
case refine_2.inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ s ∈ {s | LFunction χ s ≠ 0}

Tactic:
exact hs χ

Result:
no goals

Proof state:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ∈ {1}ᶜ
⊢ ContinuousOn (fun s => -deriv (LFunction χ) s / LFunction χ s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
replace hχ : χ ≠ 1 := by simpa only [ne_eq, Finset.mem_compl, Finset.mem_singleton] using hχ

Result:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
⊢ ContinuousOn (fun s => -deriv (LFunction χ) s / LFunction χ s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Proof state:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
this : 1 ≠ 1 ∨ s ≠ 1 → 1 ≤ s.re → LFunction 1 s ≠ 0
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}

Tactic:
tauto

Result:
no goals

Proof state:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ s ∈ {s | LFunction χ s ≠ 0}

Tactic:
simp only [ne_eq, Set.mem_setOf_eq] at hs

Result:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ s ∈ {s | LFunction χ s ≠ 0}

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn
    (fun s =>
      (↑q.totient)⁻¹ *
        (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
          -∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s))
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
refine continuousOn_const.mul <| ContinuousOn.add ?_ ?_

Result:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s => -deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s => -∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Proof state:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ s ∈ {s | LFunction χ s ≠ 0}

Tactic:
rcases hs with rfl | hs

Result:
case refine_2.inl
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
⊢ 1 ∈ {s | LFunction χ s ≠ 0}

case refine_2.inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ s ∈ {s | LFunction χ s ≠ 0}

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ∈ {1}ᶜ
⊢ χ ≠ 1

Tactic:
simpa only [ne_eq, Finset.mem_compl, Finset.mem_singleton] using hχ

Result:
no goals

Proof state:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}

Tactic:
have := LFunction_ne_zero_of_one_le_re (1 : DirichletCharacter ℂ q) (s := s)

Result:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
this : 1 ≠ 1 ∨ s ≠ 1 → 1 ≤ s.re → LFunction 1 s ≠ 0
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}

Proof state:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s => -∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
simp only [← Finset.sum_neg_distrib, mul_div_assoc, ← mul_neg, ← neg_div]

Result:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s => ∑ x ∈ {1}ᶜ, x a⁻¹ * (-deriv (LFunction x) s / LFunction x s))
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Proof state:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s => -deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
refine (continuousOn_neg_logDeriv_LFunctionTrivChar₁ q).mono fun s hs ↦ ?_

Result:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (LFunctionResidueClassAux a) {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
rw [show LFunctionResidueClassAux a = fun s ↦ _ from rfl]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s => LFunctionResidueClassAux a s) {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Proof state:
case refine_2.inl
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
⊢ 1 ∈ {s | LFunction χ s ≠ 0}

Tactic:
simp only [ne_eq, Set.mem_setOf_eq, one_re, le_refl,
  LFunction_ne_zero_of_one_le_re χ (.inl hχ), not_false_eq_true]

Result:
no goals

Proof state:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
⊢ ContinuousOn (fun s => -deriv (LFunction χ) s / LFunction χ s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
refine (continuousOn_neg_logDeriv_LFunction_of_nontriv hχ).mono fun s hs ↦ ?_

Result:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ s ∈ {s | LFunction χ s ≠ 0}

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s => LFunctionResidueClassAux a s) {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
simp only [LFunctionResidueClassAux, sub_eq_add_neg]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn
    (fun s =>
      (↑q.totient)⁻¹ *
        (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
          -∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s))
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Proof state:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
this : 1 ≠ 1 ∨ s ≠ 1 → 1 ≤ s.re → LFunction 1 s ≠ 0
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}

Tactic:
simp only [ne_eq, Set.mem_setOf_eq] at hs

Result:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
this : 1 ≠ 1 ∨ s ≠ 1 → 1 ≤ s.re → LFunction 1 s ≠ 0
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}