awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
n : ℕ
h : n ≠ 0
⊢ HSMul.hSMul (α := ℂ) (β := ℕ → ℂ) (↑q.totient : ℂ) (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) n =
    (∑ i : DirichletCharacter ℂ q,
        HSMul.hSMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ)
          (HMul.hMul (α := ℕ → ℂ) (fun (n : ℕ) ↦ (i : (a : ZMod q) → ℂ) (↑n : ZMod q)) fun (n : ℕ) ↦
            (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)))
      n

Tactic:
simp only [Pi.smul_apply, residueClass_apply ha, smul_eq_mul, ← mul_assoc,
    mul_inv_cancel_of_invertible, one_mul, Finset.sum_apply, Pi.mul_apply]

Premises used: mul_inv_cancel_of_invertible, Pi.mul_apply, mul_assoc, ArithmeticFunction.vonMangoldt.residueClass_apply, Finset.sum_apply, smul_eq_mul, one_mul, Pi.smul_apply
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
⊢ ContinuousOn (Y := ℂ)
    (fun (s : ℂ) ↦
      (↑q.totient : ℂ)⁻¹ *
        (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
          -∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s))
    {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

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

Premises used: continuousOn_const, ContinuousOn.add, ContinuousOn.mul
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
refine_1 :
  ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s)
    {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
refine_2 :
  ContinuousOn (Y := ℂ)
    (fun (s : ℂ) ↦
      -∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s)
    {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ ContinuousOn (Y := ℂ)
    (fun (s : ℂ) ↦
      (↑q.totient : ℂ)⁻¹ *
        (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
          -∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s))
    {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

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

Premises used: continuousOn_const, ContinuousOn.add, ContinuousOn.mul
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
⊢ ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s)
    {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

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

Premises used: ContinuousOn.mono, DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
refine_1 :
  ∀ (s : ℂ) (hs : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0} s),
    Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar q s ≠ 0} s
⊢ ContinuousOn (Y := ℂ) (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 ↦ ?_

Premises used: ContinuousOn.mono, DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
s : ℂ
hs : s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
refine_1 : ∀ (hs : s = 1), Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar q s ≠ 0} s
refine_1₁ :
  ∀ (hs : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0),
    Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar q s ≠ 0} s
refine_1₂ : ∀ (hs : s = 1), Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar q s ≠ 0} s
refine_1₃ :
  ∀ (hs : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0),
    Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar q s ≠ 0} s
refine_1₄ : ∀ (hs : s = 1), ¬s = 1 → LFunctionTrivChar q s ≠ 0
refine_1₅ : ∀ (hs : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0), ¬s = 1 → LFunctionTrivChar q s ≠ 0
refine_1₆ : ∀ (hs : s = 1), ¬s = 1 → LFunctionTrivChar q s = 0 → False
refine_1₇ refine_1₈ refine_1₉ refine_1₁₀ refine_1₁₁ refine_1₁₂ refine_1₁₃ refine_1₁₄ :
  ∀ (hs : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0), ¬s = 1 → LFunctionTrivChar q s = 0 → False
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ LFunctionTrivChar q s ≠ 0} s

Tactic:
tauto
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
refine_2 :
  ContinuousOn (Y := ℂ)
    (fun (s : ℂ) ↦
      ∑ x ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (-deriv (LFunction x) s / LFunction x s))
    {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ ContinuousOn (Y := ℂ)
    (fun (s : ℂ) ↦
      -∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) 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]

Premises used: neg_div, mul_div_assoc, Finset.sum_neg_distrib, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
⊢ ContinuousOn (Y := ℂ)
    (fun (s : ℂ) ↦
      ∑ x ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (-deriv (LFunction x) s / LFunction x s))
    {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
continuousOn_finsetSum _ fun χ hχ ↦ continuousOn_const.mul ?_

Premises used: continuousOn_const, continuousOn_finsetSum, ContinuousOn.mul
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
refine_2 :
  ∀ (χ : DirichletCharacter ℂ q) (hχ : Membership.mem (γ := Finset (DirichletCharacter ℂ q)) {1}ᶜ χ),
    ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -deriv (LFunction χ) s / LFunction χ s)
      {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ ContinuousOn (Y := ℂ)
    (fun (s : ℂ) ↦
      ∑ x ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (-deriv (LFunction x) s / LFunction x s))
    {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

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

Premises used: continuousOn_const, continuousOn_finsetSum, ContinuousOn.mul
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
χ : DirichletCharacter ℂ q
hχ : Membership.mem (γ := Finset (DirichletCharacter ℂ q)) {1}ᶜ χ
⊢ χ ≠ 1

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

Premises used: Finset.mem_singleton, Finset.mem_compl, ne_eq
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
χ : DirichletCharacter ℂ q
hχ : Membership.mem (γ := Finset (DirichletCharacter ℂ q)) {1}ᶜ χ
⊢ χ ≠ 1

Tactic:
replace hχ : χ ≠ 1 := by simpa only [ne_eq, Finset.mem_compl, Finset.mem_singleton] using hχ
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
⊢ ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -deriv (LFunction χ) s / LFunction χ s)
    {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

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

Premises used: DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv, ContinuousOn.mono
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
refine_2 :
  ∀ (s : ℂ) (hs : Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0} s),
    Membership.mem (γ := Set ℂ) {s : ℂ | LFunction χ s ≠ 0} s
⊢ ContinuousOn (Y := ℂ) (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 ↦ ?_

Premises used: DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv, ContinuousOn.mono
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
refine_2 : Membership.mem (γ := Set ℂ) {s : ℂ | LFunction χ s ≠ 0} 1
refine_2₁ :
  ∀ (hs : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0), Membership.mem (γ := Set ℂ) {s : ℂ | LFunction χ s ≠ 0} s
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | LFunction χ s ≠ 0} s

Tactic:
rcases hs with rfl | hs

Premises used: rfl
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | LFunction χ s ≠ 0} 1

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]

Premises used: le_refl, DirichletCharacter.LFunction_ne_zero_of_one_le_re, Set.mem_setOf_eq, ne_eq, Or.inl, not_false_eq_true, Complex.one_re
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | LFunction χ s ≠ 0} s

Tactic:
hs χ

Premises used: Set.Mem, setOf, Not
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | LFunction χ s ≠ 0} s

Tactic:
exact hs χ
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
⊢ ContinuousOn (LFunctionResidueClassAux a) {s : ℂ | 1 ≤ s.re}

Tactic:
(continuousOn_LFunctionResidueClassAux' a).mono fun s hs ↦ ?_

Premises used: ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux', ContinuousOn.mono
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
refine :
  ∀ (s : ℂ) (hs : Membership.mem (γ := Set ℂ) {s : ℂ | 1 ≤ s.re} s),
    Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0} s
⊢ ContinuousOn (LFunctionResidueClassAux a) {s : ℂ | 1 ≤ s.re}

Tactic:
refine (continuousOn_LFunctionResidueClassAux' a).mono fun s hs ↦ ?_

Premises used: ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux', ContinuousOn.mono
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
s : ℂ
hs : Membership.mem (γ := Set ℂ) {s : ℂ | 1 ≤ s.re} s
inl :
  ∀ (hs : Membership.mem (γ := Set ℂ) {s : ℂ | 1 ≤ s.re} 1),
    Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0} 1
inr : ∀ (hs₁ : s ≠ 1), Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0} s
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0} s

Tactic:
rcases eq_or_ne s 1 with rfl | hs₁

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
hs : Membership.mem (γ := Set ℂ) {s : ℂ | 1 ≤ s.re} 1
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0} 1

Tactic:
simp only [ne_eq, Set.mem_setOf_eq, true_or]

Premises used: true_or, Set.mem_setOf_eq, ne_eq
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
s : ℂ
hs : Membership.mem (γ := Set ℂ) {s : ℂ | 1 ≤ s.re} s
hs₁ : s ≠ 1
inr : ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0} s

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

Premises used: Set.mem_setOf_eq, false_or, ne_eq
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
s : ℂ
hs : Membership.mem (γ := Set ℂ) {s : ℂ | 1 ≤ s.re} s
hs₁ : s ≠ 1
⊢ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0

Tactic:
fun χ ↦ LFunction_ne_zero_of_one_le_re χ (.inr hs₁) <| Set.mem_setOf.mp hs

Premises used: DirichletCharacter.LFunction_ne_zero_of_one_le_re, Set.mem_setOf, Iff.mp, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
s : ℂ
hs : Membership.mem (γ := Set ℂ) {s : ℂ | 1 ≤ s.re} s
hs₁ : s ≠ 1
⊢ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0

Tactic:
exact fun χ ↦ LFunction_ne_zero_of_one_le_re χ (.inr hs₁) <| Set.mem_setOf.mp hs

Premises used: DirichletCharacter.LFunction_ne_zero_of_one_le_re, Set.mem_setOf, Iff.mp, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : Membership.mem (γ := Set ℂ) {s : ℂ | 1 < s.re} s
⊢ 1 < s.re

Tactic:
replace hs := Set.mem_setOf.mp hs
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
simp :
  (↑q.totient : ℂ)⁻¹ *
      (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s -
        ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s) =
    HMul.hMul (α := ℂ) (-(↑q.totient : ℂ)⁻¹)
        (∑ χ : DirichletCharacter ℂ q,
          HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s / LFunction χ s)) -
      (↑q.totient : ℂ)⁻¹ / (s - 1)
⊢ 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]

Premises used: ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
rw :
  -(↑q.totient : ℂ)⁻¹ *
      (deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
        ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s) =
    -(↑q.totient : ℂ)⁻¹ *
      (∑ χ : DirichletCharacter ℂ q,
          HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s / LFunction χ s) +
        1 / (s - 1))
⊢ (↑q.totient : ℂ)⁻¹ *
      (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s -
        ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s) =
    HMul.hMul (α := ℂ) (-(↑q.totient : ℂ)⁻¹)
        (∑ χ : DirichletCharacter ℂ q,
          HMul.hMul (α := ℂ) ((χ : (a : ZMod 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]

Premises used: neg_div, sub_eq_add_neg, Nat.totient, Nat.cast, neg_add', Inv.inv, div_eq_mul_one_div, mul_add, neg_mul, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
congrm :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    ∑ χ : DirichletCharacter ℂ q,
        HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s / LFunction χ s) +
      1 / (s - 1)
⊢ -(↑q.totient : ℂ)⁻¹ *
      (deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
        ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s) =
    -(↑q.totient : ℂ)⁻¹ *
      (∑ χ : DirichletCharacter ℂ q,
          HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s / LFunction χ s) +
        1 / (s - 1))

Tactic:
congrm (_ * ?_)

Premises used: HMul.hMul
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ IsUnit a⁻¹

Tactic:
have ha' : IsUnit a⁻¹ := isUnit_of_dvd_one ⟨a, (ZMod.inv_mul_of_unit a ha).symm⟩
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
rw :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1) +
      ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s)
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    ∑ χ : DirichletCharacter ℂ q,
        HMul.hMul (α := ℂ) ((χ : (a : ZMod 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]

Premises used: add_right_comm, MulChar.one_apply, OfNat.ofNat, Fintype.sum_eq_add_sum_compl, one_mul
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
simp :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ x ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction x) s / LFunction x s) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1) +
      ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s)
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1) +
      ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s)

Tactic:
simp only [mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
congrm :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ x ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction x) s / LFunction x s) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1) +
      ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s)

Tactic:
congrm (?_ + _)

Premises used: HAdd.hAdd
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ s ≠ 1

Tactic:
have hs₁ : s ≠ 1 := fun h ↦ ((h ▸ hs).trans_eq one_re).false
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
rw :
  deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s +
      LFunction (N := q) 1 s / ((s - 1) * LFunction (N := q) 1 s) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)

Tactic:
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₁)]

Premises used: DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_one, DirichletCharacter.LFunctionTrivChar₁, sub_ne_zero_of_ne, mul_div_mul_left, DirichletCharacter.LFunctionTrivChar, add_div, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
enter : LFunction (N := q) 1 s
| deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + LFunction (N := q) 1 s / ((s - 1) * LFunction (N := q) 1 s)

Tactic:
enter [2, 1]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
rw : LFunction (N := q) 1 s * 1
| LFunction (N := q) 1 s

Tactic:
rw [← mul_one (LFunction ..)]

Premises used: DirichletCharacter.LFunction, mul_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
enter : LFunction (N := q) 1 s * 1
| deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + LFunction (N := q) 1 s / ((s - 1) * LFunction (N := q) 1 s)

Tactic:
enter [2, 1]; rw [← mul_one (LFunction ..)]

Premises used: DirichletCharacter.LFunction, mul_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
conv_lhs :
  deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s +
      LFunction (N := q) 1 s * 1 / ((s - 1) * LFunction (N := q) 1 s) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)
⊢ deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s +
      LFunction (N := q) 1 s / ((s - 1) * LFunction (N := q) 1 s) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)

Tactic:
conv_lhs => enter [2, 1]; rw [← mul_one (LFunction ..)]

Premises used: DirichletCharacter.LFunction, mul_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
rw :
  deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s +
      1 * LFunction (N := q) 1 s / ((s - 1) * LFunction (N := q) 1 s) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)
rw₁ rw₂ :
  deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)
⊢ deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s +
      LFunction (N := q) 1 s * 1 / ((s - 1) * LFunction (N := q) 1 s) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 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]

Premises used: mul_div_mul_right, LT.lt.le, DirichletCharacter.LFunction_ne_zero_of_one_le_re, mul_comm, OfNat.ofNat, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
rw :
  (fun (s : ℂ) ↦ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s - (↑q.totient : ℂ)⁻¹ / (s - 1)) (↑x : ℂ) =
    (↑(re ((fun (s : ℂ) ↦ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s - (↑q.totient : ℂ)⁻¹ / (s - 1)) (↑x : ℂ))) : ℂ)
⊢ LFunctionResidueClassAux a (↑x : ℂ) = (↑(LFunctionResidueClassAux a (↑x : ℂ)).re : ℂ)

Tactic:
rw [eqOn_LFunctionResidueClassAux ha hx]

Premises used: ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
simp :
  L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) - (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) =
    (↑(L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ)).re : ℂ) - (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
⊢ (fun (s : ℂ) ↦ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s - (↑q.totient : ℂ)⁻¹ / (s - 1)) (↑x : ℂ) =
    (↑(re ((fun (s : ℂ) ↦ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) s - (↑q.totient : ℂ)⁻¹ / (s - 1)) (↑x : ℂ))) : ℂ)

Tactic:
simp only [sub_re, ofReal_sub]

Premises used: Complex.sub_re, Complex.ofReal_sub