awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℂ)
e_a₁ : (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).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 : ℂ)

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 < x
⊢ 1 < (↑(↑x : ℂ).re : EReal)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
e_a :
  ∑' (n : ℕ), term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
    (↑(∑' (a_1 : ℕ), (term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) a_1).re) : ℂ)
⊢ L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) =
    (↑(L (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ)).re : ℂ)

Tactic:
rw [LSeries, re_tsum <| LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| by norm_cast]

Premises used: ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one, LSeries, LSeriesSummable_of_abscissaOfAbsConv_lt_re, Complex.re_tsum, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
e_a :
  Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n)
    (∑' (a_1 : ℕ), (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) a_1).re : ℂ))
⊢ ∑' (n : ℕ), term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
    (↑(∑' (a_1 : ℕ), (term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) a_1).re) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℂ))

Tactic:
tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
e_a :
  ∀ (n : ℕ),
    term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
      (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n).re : ℂ)
⊢ Eq (α := ℂ) (∑' (n : ℕ), term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n)
    (∑' (a_1 : ℕ), (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) a_1).re : ℂ))

Tactic:
refine tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℂ)
e_a₁ :
  ∀ (hn : n ≠ 0),
    term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
      (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n).re : ℂ)
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) 0 =
    (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) 0).re : ℂ)

Tactic:
simp only [term_zero, zero_re, ofReal_zero]

Premises used: Complex.ofReal_zero, Complex.zero_re, LSeries.term_zero
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
hn : n ≠ 0
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n =
    (↑(term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑x : ℂ) n).re : ℂ)

Tactic:
simp only [term_of_ne_zero hn, ← ofReal_natCast n, ← ofReal_cpow n.cast_nonneg, ← ofReal_div,
        ofReal_re]

Premises used: Nat.cast_nonneg, Complex.ofReal_cpow, LSeries.term_of_ne_zero, Complex.ofReal_natCast, Complex.ofReal_div, Complex.ofReal_re
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℂ)
e_a₅ e_a₆ : (↑((↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ) = (↑((↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ)
⊢ (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1) = (↑((↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)).re : ℂ)

Tactic:
rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
      ← ofReal_div, ofReal_re]

Premises used: Complex.ofReal_one, Complex.ofReal_natCast, Complex.ofReal_div, Complex.ofReal_re, Complex.ofReal_sub, Complex.ofReal_inv
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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)

Tactic:
ofReal_injective ?_

Premises used: Complex.ofReal_injective
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
refine :
  (↑(∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ) =
    (↑((LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)) : ℂ)
⊢ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x =
    (LFunctionResidueClassAux a (↑x : ℂ)).re + (↑q.totient : ℝ)⁻¹ / (x - 1)

Tactic:
refine ofReal_injective ?_

Premises used: Complex.ofReal_injective
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
simp :
  ∑' (a_1 : ℕ), (↑(residueClass a a_1) : ℂ) / HPow.hPow (α := ℂ) (↑a_1 : ℂ) (↑x : ℂ) =
    (↑(LFunctionResidueClassAux a (↑x : ℂ)).re : ℂ) + (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)
⊢ (↑(∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) 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]

Premises used: Nat.cast_nonneg, Complex.ofReal_cpow, Complex.ofReal_add, Complex.ofReal_one, Complex.ofReal_natCast, Complex.ofReal_div, Complex.ofReal_sub, Complex.ofReal_tsum, Complex.ofReal_inv
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
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 : ℂ))
⊢ ∑' (a_1 : ℕ), (↑(residueClass a a_1) : ℂ) / HPow.hPow (α := ℂ) (↑a_1 : ℂ) (↑x : ℂ) =
    (↑(LFunctionResidueClassAux a (↑x : ℂ)).re : ℂ) + (↑q.totient : ℂ)⁻¹ / ((↑x : ℂ) - 1)

Tactic:
simp_rw [← LFunctionResidueClassAux_real ha hx,
      eqOn_LFunctionResidueClassAux ha <| Set.mem_setOf.mpr (ofReal_re x ▸ hx), sub_add_cancel,
      LSeries, term]

Premises used: Iff.mpr, Set.mem_setOf, LSeries, ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux_real, LSeries.term, sub_add_cancel, ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℂ))

Tactic:
tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
refine :
  ∀ (n : ℕ),
    (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) =
      if n = 0 then 0 else (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑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 : ℂ))

Tactic:
refine tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
neg :
  ∀ (hn : ¬n = 0),
    (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) =
      (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
⊢ (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) =
    if n = 0 then 0 else (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)

Tactic:
split_ifs with hn
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
hn : n = 0
⊢ (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) = 0

Tactic:
simp only [hn, residueClass_apply_zero, ofReal_zero, zero_div]

Premises used: zero_div, Complex.ofReal_zero, ArithmeticFunction.vonMangoldt.residueClass_apply_zero
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
inst : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
hn : ¬n = 0
⊢ (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) =
    (↑(residueClass a n) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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)

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
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc 1 2) x
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | 1 ≤ s.re} (↑x : ℂ)

Tactic:
simpa only [Set.mem_setOf_eq, ofReal_re] using hx.1

Premises used: Set.mem_setOf_eq, And.left, Complex.ofReal_re
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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)
⊢ 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
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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)
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
⊢ ∃ (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

Premises used: bddBelow_def, CompactIccSpace.isCompact_Icc, Iff.mp, IsCompact.bddBelow_image
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ ∀ {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
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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

Tactic:
⟨-C, fun {x} hx ↦ ?_⟩

Premises used: Exists.intro, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
refine :
  ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Set.Ioc 1 2) x),
    (↑q.totient : ℝ)⁻¹ / (x - 1) - -C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ ∃ (C : ℝ),
    ∀ {x : ℝ},
      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 ↦ ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
rw : C ≤ (LFunctionResidueClassAux a (↑x : ℂ)).re
⊢ (↑q.totient : ℝ)⁻¹ / (x - 1) - -C ≤ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x

Tactic:
rw [H hx.1, add_comm, sub_neg_eq_add, add_le_add_iff_left]

Premises used: add_le_add_iff_left, add_comm, And.left, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ C ≤ (LFunctionResidueClassAux a (↑x : ℂ)).re

Tactic:
hC <| Set.mem_Icc_of_Ioc hx

Premises used: Set.mem_Icc_of_Ioc
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ C ≤ (LFunctionResidueClassAux a (↑x : ℂ)).re

Tactic:
exact hC <| Set.mem_Icc_of_Ioc hx

Premises used: Set.mem_Icc_of_Ioc
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 (b : ℕ) ↦
    (if Nat.Prime b then 0 else residueClass a b) / (↑b : ℝ) + (if Nat.Prime b then residueClass a b else 0) / (↑b : ℝ)

Tactic:
(summable_residueClass_non_primes_div a).add H

Premises used: ArithmeticFunction.vonMangoldt.summable_residueClass_non_primes_div, Summable.add
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℝ)
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 : ℝ)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / (↑n : ℝ)

Tactic:
convert! (summable_residueClass_non_primes_div a).add H using 2 with n

Premises used: ArithmeticFunction.vonMangoldt.summable_residueClass_non_primes_div, Summable.add
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℝ)
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:
simp only [← add_div, ite_add_ite, zero_add, add_zero, ite_self]

Premises used: ite_self, zero_add, add_zero, ite_add_ite, add_div
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℝ)

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]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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

Tactic:
Summable.tsum_le_tsum (fun n ↦ ?_) ?_ key

Premises used: Summable.tsum_le_tsum
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℝ)
refine_2 : Summable (α := ℝ) fun (n : ℕ) ↦ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ ∑' (n : ℕ), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ C

Tactic:
refine Summable.tsum_le_tsum (fun n ↦ ?_) ?_ key

Premises used: Summable.tsum_le_tsum
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℕ
refine_1 : residueClass a 0 / HPow.hPow (α := ℝ) (↑0 : ℝ) x ≤ residueClass a 0 / (↑0 : ℝ)
refine_1₁ : ∀ (hn : n > 0), residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)
⊢ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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
⊢ residueClass a 0 / HPow.hPow (α := ℝ) (↑0 : ℝ) x ≤ residueClass a 0 / (↑0 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℕ
hn : n > 0
⊢ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)

Tactic:
div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, ArithmeticFunction.vonMangoldt.residueClass_nonneg, LT.lt, div_le_div_of_nonneg_left, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℕ
hn : n > 0
refine_1 : (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ residueClass a n / HPow.hPow (α := ℝ) (↑n : ℝ) x ≤ residueClass a n / (↑n : ℝ)

Tactic:
refine div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_

Premises used: ArithmeticFunction.vonMangoldt.residueClass_nonneg, div_le_div_of_nonneg_left
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
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 : ℕ
hn : n > 0
rw : HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
| (↑n : ℝ)

Tactic:
rw [← Real.rpow_one n]

Premises used: Nat.cast, Real.rpow_one