awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
classical :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s) +
        ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s) +
      1 / (s - 1)
classical₁ :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    1 * (deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s) +
        ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s) +
      1 / (s - 1)
classical₂ :
  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 +
        ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s) +
      1 / (s - 1)
classical₃ classical₄ classical₅ :
  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)
classical₆ :
  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 =
    ∑ χ : DirichletCharacter ℂ q,
        HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s / LFunction χ s) +
      1 / (s - 1)
have classical₇ : deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s =
  deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)
Tactic: classical -- for `Fintype.sum_eq_add_sum_compl`
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ LFunctionResidueClassAux a (↑x : ℂ) = (↑(LFunctionResidueClassAux a (↑x : ℂ)).re : ℂ)
have 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 : ℂ))) : ℂ)
Tactic: rw [eqOn_LFunctionResidueClassAux ha hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (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 : ℂ))) : ℂ)
have 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 : ℂ)
Tactic: simp only [sub_re, ofReal_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) - (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) =
    (↑(L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ)).re : ℂ) - (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
have e_a : L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) = (↑(L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ)).re : ℂ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
e_a :
  L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) =
    (↑(L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ)).re : ℂ)
⊢ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) - (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) =
    (↑(L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ)).re : ℂ) - (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
have e_a₁ : (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) =
    (↑(L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ)).re : ℂ)
have e_a : ∑' (n : ℕ), term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
  (↑(∑' (a_1 : ℕ), (term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) a_1).re) : ℂ)
Tactic: rw [LSeries, re_tsum <| LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| by norm_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
    (↑(∑' (a_1 : ℕ), (term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) a_1).re) : ℂ)
have e_a : Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n)
  (∑' (a_1 : ℕ), (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) a_1).re : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n)
    (∑' (a_1 : ℕ), (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) a_1).re : ℂ))
have e_a : ∀ (n : ℕ),
  term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
    (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n).re : ℂ)
Tactic: refine tsum_congr fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
    (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n).re : ℂ)
have e_a : term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) 0 =
  (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) 0).re : ℂ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
e_a :
  term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) 0 =
    (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) 0).re : ℂ)
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
    (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n).re : ℂ)
have e_a₁ : ∀ (hn : n ≠ 0),
  term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
    (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n).re : ℂ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
have e_a : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
Tactic: rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
      ← ofReal_div, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
e_a : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
⊢ (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
have e_a₁ : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ)) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ))).re : ℂ)
Tactic: rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
      ← ofReal_div, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
e_a : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
e_a₁ : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ)) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ))).re : ℂ)
⊢ (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
have e_a₂ : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / (↑(x - 1) : ℂ) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / (↑(x - 1) : ℂ)).re : ℂ)
Tactic: rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
      ← ofReal_div, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
e_a : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
e_a₁ : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ)) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ))).re : ℂ)
e_a₂ : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / (↑(x - 1) : ℂ) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / (↑(x - 1) : ℂ)).re : ℂ)
⊢ (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
have e_a₃ : (↑(↑q.totient : ℝ)⁻¹ : ℂ) / (↑(x - 1) : ℂ) = (↑((↑(↑q.totient : ℝ)⁻¹ : ℂ) / (↑(x - 1) : ℂ)).re : ℂ)
Tactic: rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
      ← ofReal_div, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
e_a : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
e_a₁ : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ)) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ))).re : ℂ)
e_a₂ : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / (↑(x - 1) : ℂ) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / (↑(x - 1) : ℂ)).re : ℂ)
e_a₃ : (↑(↑q.totient : ℝ)⁻¹ : ℂ) / (↑(x - 1) : ℂ) = (↑((↑(↑q.totient : ℝ)⁻¹ : ℂ) / (↑(x - 1) : ℂ)).re : ℂ)
⊢ (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
have e_a₄ : (↑((↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ) = (↑(↑((↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ).re : ℂ)
Tactic: rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
      ← ofReal_div, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
e_a : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
e_a₁ : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ)) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / ((↑x : ℂ) - (↑1 : ℂ))).re : ℂ)
e_a₂ : (↑(↑q.totient : ℝ) : ℂ)⁻¹ / (↑(x - 1) : ℂ) = (↑((↑(↑q.totient : ℝ) : ℂ)⁻¹ / (↑(x - 1) : ℂ)).re : ℂ)
e_a₃ : (↑(↑q.totient : ℝ)⁻¹ : ℂ) / (↑(x - 1) : ℂ) = (↑((↑(↑q.totient : ℝ)⁻¹ : ℂ) / (↑(x - 1) : ℂ)).re : ℂ)
e_a₄ : (↑((↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ) = (↑(↑((↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ).re : ℂ)
⊢ (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)
have e_a₅ : (↑((↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ) = (↑((↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ)
Tactic: rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
      ← ofReal_div, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x =
    (LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)
have refine : (↑(∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ) =
  (↑((LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ)
Tactic: refine ofReal_injective ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (↑(∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ) =
    (↑((LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ)
have simp : ∑' (a_1 : ℕ), (↑(residueClass a a_1) : ℂ) / HPow.hPow (α := ℂ) (↑a_1 : ℂ) (↑x : ℂ) =
  (↑(LFunctionResidueClassAux a (↑x : ℂ)).re : ℂ) + (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)
Tactic: simp only [ofReal_tsum, ofReal_div, ofReal_cpow (Nat.cast_nonneg _), ofReal_natCast,
      ofReal_add, ofReal_inv, ofReal_sub, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (a_1 : ℕ), (↑(residueClass a a_1) : ℂ) / HPow.hPow (α := ℂ) (↑a_1 : ℂ) (↑x : ℂ) =
    (↑(LFunctionResidueClassAux a (↑x : ℂ)).re : ℂ) + (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)
have simp_rw : Eq (α := ℂ) (∑' (a_1 : ℕ), (↑(residueClass a a_1) : ℂ) / HPow.hPow (α := ℂ) (↑a_1 : ℂ) (↑x : ℂ))
  (∑' (n : ℕ), if n = 0 then 0 else (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ))
Tactic: simp_rw [← LFunctionResidueClassAux_real ha hx,
      eqOn_LFunctionResidueClassAux ha <| Set.mem_setOf.mpr (ofReal_re x ▸ hx), sub_add_cancel,
      LSeries, term]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ Eq (α := ℂ) (∑' (a_1 : ℕ), (↑(residueClass a a_1) : ℂ) / HPow.hPow (α := ℂ) (↑a_1 : ℂ) (↑x : ℂ))
    (∑' (n : ℕ), if n = 0 then 0 else (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ))
have refine : ∀ (n : ℕ),
  (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) =
    if n = 0 then 0 else (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
Tactic: refine tsum_congr fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
⊢ (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) =
    if n = 0 then 0 else (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
have pos : ∀ (hn : n = 0), (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) = 0
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
pos : ∀ (hn : n = 0), (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) = 0
⊢ (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) =
    if n = 0 then 0 else (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
have neg : ∀ (hn : ¬n = 0),
  (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) =
    (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
⊢ ∃ (C : ℝ),
    ∀ {x : ℝ},
      Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
        (↑q.totient : ℝ)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have H : ∀ {x : ℝ} (hx : 1 < x),
  ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x =
    (LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)
Tactic: have H {x : ℝ} (hx : 1 < x) :
      ∑' n, residueClass a n / (n : ℝ) ^ x =
        (LFunctionResidueClassAux a x).re + (q.totient : ℝ)⁻¹ / (x - 1) := by
    refine ofReal_injective ?_
    simp only [ofReal_tsum, ofReal_div, ofReal_cpow (Nat.cast_nonneg _), ofReal_natCast,
      ofReal_add, ofReal_inv, ofReal_sub, ofReal_one]
    simp_rw [← LFunctionResidueClassAux_real ha hx,
      eqOn_LFunctionResidueClassAux ha <| Set.mem_setOf.mpr (ofReal_re x ▸ hx), sub_add_cancel,
      LSeries, term]
    refine tsum_congr fun n ↦ ?_
    split_ifs with hn
    · simp only [hn, residueClass_apply_zero, ofReal_zero, zero_div]
    · rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ} (hx : 1 < x),
    ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x =
      (LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)
⊢ ∃ (C : ℝ),
    ∀ {x : ℝ},
      Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
        (↑q.totient : ℝ)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (LFunctionResidueClassAux a (↑x : ℂ)).re) (Set.Icc 1 2)
Tactic: have : ContinuousOn (fun x : ℝ ↦ (LFunctionResidueClassAux a x).re) (Set.Icc 1 2) :=
    continuous_re.continuousOn.comp (t := Set.univ) (continuousOn_LFunctionResidueClassAux a)
      (fun ⦃x⦄ a ↦ trivial) |>.comp continuous_ofReal.continuousOn fun x hx ↦ by
        simpa only [Set.mem_setOf_eq, ofReal_re] using hx.1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ} (hx : 1 < x),
    ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x =
      (LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (LFunctionResidueClassAux a (↑x : ℂ)).re) (Set.Icc 1 2)
⊢ ∃ (C : ℝ),
    ∀ {x : ℝ},
      Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
        (↑q.totient : ℝ)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have obtain : ∀ (C : ℝ)
  (hC :
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ (LFunctionResidueClassAux a (↑x : ℂ)).re) '' Set.Icc 1 2) y → C ≤ y),
  ∃ (C : ℝ),
    ∀ {x : ℝ},
      Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
        (↑q.totient : ℝ)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
Tactic: obtain ⟨C, hC⟩ := bddBelow_def.mp <| IsCompact.bddBelow_image isCompact_Icc this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ} (hx : 1 < x),
    ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x =
      (LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (LFunctionResidueClassAux a (↑x : ℂ)).re) (Set.Icc 1 2)
C : ℝ
hC :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ (LFunctionResidueClassAux a (↑x : ℂ)).re) '' Set.Icc 1 2) y → C ≤ y
⊢ ∃ (C : ℝ),
    ∀ {x : ℝ},
      Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
        (↑q.totient : ℝ)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have hC₁ : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Icc 1 2) x), C ≤ (LFunctionResidueClassAux a (↑x : ℂ)).re
Tactic: replace hC {x : ℝ} (hx : x ∈ Set.Icc 1 2) : C ≤ (LFunctionResidueClassAux a x).re :=
    hC (LFunctionResidueClassAux a x).re <|
      Set.mem_image_of_mem (fun x : ℝ ↦ (LFunctionResidueClassAux a x).re) hx
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ} (hx : 1 < x),
    ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x =
      (LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (LFunctionResidueClassAux a (↑x : ℂ)).re) (Set.Icc 1 2)
C : ℝ
hC : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Icc 1 2) x), C ≤ (LFunctionResidueClassAux a (↑x : ℂ)).re
⊢ ∃ (C : ℝ),
    ∀ {x : ℝ},
      Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x →
        (↑q.totient : ℝ)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have refine : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x),
  (↑q.totient : ℝ)⁻¹ / (x - 1) - -C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
Tactic: refine ⟨-C, fun {x} hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ} (hx : 1 < x),
    ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x =
      (LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (LFunctionResidueClassAux a (↑x : ℂ)).re) (Set.Icc 1 2)
C : ℝ
hC : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Icc 1 2) x), C ≤ (LFunctionResidueClassAux a (↑x : ℂ)).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x
⊢ (↑q.totient : ℝ)⁻¹ / (x - 1) - -C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have rw : C ≤ (LFunctionResidueClassAux a (↑x : ℂ)).re
Tactic: rw [H hx.1, add_comm, sub_neg_eq_add, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
have h : ∀ (n : ℕ),
  residueClass a n / (↑n : ℝ) =
    (if Nat.Prime n then 0 else residueClass a n) / (↑n : ℝ) + (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
Tactic: convert! (summable_residueClass_non_primes_div a).add H using 2 with n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (hypothesis)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
⊢ False
have key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
Tactic: have key : Summable fun n : ℕ ↦ residueClass a n / n := by
    convert! (summable_residueClass_non_primes_div a).add H using 2 with n
    simp only [← add_div, ite_add_ite, zero_add, add_zero, ite_self]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
have refine_1 : ∀ (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)
Tactic: refine Summable.tsum_le_tsum (fun n ↦ ?_) ?_ key
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable (α := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ)
key : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)
C : ℝ := ∑' (n : ℕ), residueClass a n / (↑n : ℝ)
x : ℝ
hx : 1 < x
refine_1 : ∀ (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)
⊢ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C
have refine_2 : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
Tactic: refine Summable.tsum_le_tsum (fun n ↦ ?_) ?_ key