-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The auxiliary function agrees on `re s > 1` with the L-series of the von Mangoldt function
restricted to the residue class `a : ZMod q` minus the principal part `(q.totient)⁻¹/(s-1)`
of its pole at `s = 1`. -/
lemma eqOn_LFunctionResidueClassAux (ha : IsUnit a) :
    Set.EqOn (LFunctionResidueClassAux a)
      (fun s ↦ L ↗(residueClass a) s - (q.totient : ℂ)⁻¹ / (s - 1))
      {s | 1 < s.re}

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) + 1 / (s - 1)

Tactic:
classical rw [Fintype.sum_eq_add_sum_compl 1, MulChar.one_apply ha', one_mul, add_right_comm]
simp only [mul_div_assoc]
congrm (?_ + _)
have hs₁ : s ≠ 1 := fun h ↦ ((h ▸ hs).trans_eq one_re).false
rw [deriv_LFunctionTrivChar₁_apply_of_ne_one _ hs₁, LFunctionTrivChar₁,
  Function.update_of_ne hs₁, LFunctionTrivChar, add_div,
  mul_div_mul_left _ _ (sub_ne_zero_of_ne hs₁)]
conv_lhs => enter [2, 1]; rw [← mul_one (LFunction ..)]
rw [mul_comm _ 1, mul_div_mul_right _ _ <| LFunction_ne_zero_of_one_le_re 1 (.inr hs₁) hs.le]

Result:
no goals

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunction 1) s / LFunction 1 s + LFunction 1 s * 1 / ((s - 1) * LFunction 1 s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Tactic:
rw [mul_comm _ 1, mul_div_mul_right _ _ <| LFunction_ne_zero_of_one_le_re 1 (.inr hs₁) hs.le]

Result:
no goals

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ x ∈ {1}ᶜ, x a⁻¹ * (deriv (LFunction x) s / LFunction x s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1) + ∑ i ∈ {1}ᶜ, i a⁻¹ * (deriv (LFunction i) s / LFunction i s)

Tactic:
congrm (?_ + _)

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s = deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ LFunctionResidueClassAux a s = (fun s => L (fun n => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) s

Tactic:
simp only [LSeries_residueClass_eq ha hs, LFunctionResidueClassAux]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ (↑q.totient)⁻¹ *
      (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s -
        ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s) =
    -(↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) -
      (↑q.totient)⁻¹ / (s - 1)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
⊢ Set.EqOn (LFunctionResidueClassAux a) (fun s => L (fun n => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1))
    {s | 1 < s.re}

Tactic:
intro s hs

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : s ∈ {s | 1 < s.re}
⊢ LFunctionResidueClassAux a s = (fun s => L (fun n => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) s

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : s ∈ {s | 1 < s.re}
⊢ LFunctionResidueClassAux a s = (fun s => L (fun n => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) s

Tactic:
replace hs := Set.mem_setOf.mp hs

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ LFunctionResidueClassAux a s = (fun s => L (fun n => ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) s

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ -(↑q.totient)⁻¹ *
      (deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
        ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s) =
    -(↑q.totient)⁻¹ * (∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) + 1 / (s - 1))

Tactic:
congrm (_ * ?_)

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) + 1 / (s - 1)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) + 1 / (s - 1)

Tactic:
have ha' : IsUnit a⁻¹ := isUnit_of_dvd_one ⟨a, (ZMod.inv_mul_of_unit a ha).symm⟩

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) + 1 / (s - 1)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) + 1 / (s - 1)

Tactic:
rw [Fintype.sum_eq_add_sum_compl 1, MulChar.one_apply ha', one_mul, add_right_comm]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1) + ∑ i ∈ {1}ᶜ, i a⁻¹ * (deriv (LFunction i) s / LFunction i s)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1) + ∑ i ∈ {1}ᶜ, i a⁻¹ * (deriv (LFunction i) s / LFunction i s)

Tactic:
simp only [mul_div_assoc]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ x ∈ {1}ᶜ, x a⁻¹ * (deriv (LFunction x) s / LFunction x s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1) + ∑ i ∈ {1}ᶜ, i a⁻¹ * (deriv (LFunction i) s / LFunction i s)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s = deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Tactic:
have hs₁ : s ≠ 1 := fun h ↦ ((h ▸ hs).trans_eq one_re).false

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s = deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ (↑q.totient)⁻¹ *
      (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s -
        ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s) =
    -(↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) -
      (↑q.totient)⁻¹ / (s - 1)

Tactic:
rw [neg_div, ← neg_add', mul_neg, ← neg_mul, div_eq_mul_one_div (q.totient : ℂ)⁻¹,
  sub_eq_add_neg, ← neg_mul, ← mul_add]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ -(↑q.totient)⁻¹ *
      (deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
        ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s) =
    -(↑q.totient)⁻¹ * (∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) + 1 / (s - 1))