awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
⊢ LocallyIntegrableOn S (Set.Ici 1) volume

Tactic:
simpa using locallyIntegrableOn_mul_sum_Icc f zero_le_one (locallyIntegrableOn_const 1)

Premises used: MeasureTheory.locallyIntegrableOn_const, zero_le_one, locallyIntegrableOn_mul_sum_Icc, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
⊢ LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume

Tactic:
have h₀ : LocallyIntegrableOn (fun t ↦ S t - l * t) (Set.Ici 1) := by
    refine .sub ?_ <| ContinuousOn.locallyIntegrableOn (by fun_prop) measurableSet_Ici
    simpa using locallyIntegrableOn_mul_sum_Icc f zero_le_one (locallyIntegrableOn_const 1)
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume

Tactic:
have h₁ : IntegrableOn (fun t ↦ ‖S t - l * t‖ * t ^ (-s - 1)) (Set.Ici 1) :=
    lemma₂ hs h₀ fun t ht ↦ (hT t ht).le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume

Tactic:
((h₀.norm.mul_continuousOn ?_ isLocallyClosed_Ici).integrableOn_compact_subset
      Set.Icc_subset_Ici_self isCompact_Icc).mono_set Set.Ioc_subset_Icc_self

Premises used: isLocallyClosed_Ici, Set.Ioc_subset_Icc_self, MeasureTheory.LocallyIntegrableOn.mul_continuousOn, CompactIccSpace.isCompact_Icc, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset, MeasureTheory.LocallyIntegrableOn.norm, Set.Icc_subset_Ici_self
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
refine : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ici 1)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume

Tactic:
refine ((h₀.norm.mul_continuousOn ?_ isLocallyClosed_Ici).integrableOn_compact_subset
      Set.Icc_subset_Ici_self isCompact_Icc).mono_set Set.Ioc_subset_Icc_self

Premises used: isLocallyClosed_Ici, Set.Ioc_subset_Icc_self, MeasureTheory.LocallyIntegrableOn.mul_continuousOn, CompactIccSpace.isCompact_Icc, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset, MeasureTheory.LocallyIntegrableOn.norm, Set.Icc_subset_Ici_self
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ici 1)

Tactic:
fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt

Premises used: Real.continuousAt_rpow_const, ContinuousAt.continuousWithinAt, HSub.hSub, LT.lt.ne', zero_lt_one, LT.lt.trans_le, ContinuousOn, Or.inl, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ici 1)

Tactic:
exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt

Premises used: Real.continuousAt_rpow_const, ContinuousAt.continuousWithinAt, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume

Tactic:
have h₂ : IntegrableOn (fun t : ℝ ↦ ‖S t - l * t‖ * (t ^ ((-1 : ℝ) - 1))) (Set.Ioc 1 T) := by
    refine ((h₀.norm.mul_continuousOn ?_ isLocallyClosed_Ici).integrableOn_compact_subset
      Set.Icc_subset_Ici_self isCompact_Icc).mono_set Set.Ioc_subset_Icc_self
    exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
rwa : -(↑s : ℂ).re < -1
rwa₁ rwa₂ rwa₃ rwa₄ : 1 < (↑s : ℂ).re
⊢ (-(↑s : ℂ)).re < -1

Tactic:
rwa [neg_re, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, Complex.neg_re
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
⊢ -(↑s : ℂ) + 1 = -((↑s : ℂ) - 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
hb : (↑s : ℂ) - 1 ≠ 0
⊢ (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1

Tactic:
rw [integral_Ioi_cpow_of_lt (by rwa [neg_re, neg_lt_neg_iff]) zero_lt_one, ofReal_one,
      one_cpow, show -(s : ℂ) + 1 = -(s - 1) by ring, neg_div_neg_eq, mul_div_cancel₀]

Premises used: Complex.ofReal_one, mul_div_cancel₀, zero_lt_one, neg_div_neg_eq, Complex.one_cpow, integral_Ioi_cpow_of_lt
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
⊢ (↑s : ℂ) - 1 ≠ 0

Tactic:
(sub_ne_zero.trans ofReal_ne_one).mpr hs.ne'

Premises used: Iff.mpr, sub_ne_zero, Complex.ofReal_ne_one, LT.lt.ne', Iff.trans
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
⊢ (↑s : ℂ) - 1 ≠ 0

Tactic:
exact (sub_ne_zero.trans ofReal_ne_one).mpr hs.ne'

Premises used: Iff.mpr, sub_ne_zero, Complex.ofReal_ne_one, LT.lt.ne', Iff.trans
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
⊢ (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1

Tactic:
have h₃ : (s - 1) * ∫ (t : ℝ) in Set.Ioi 1, (t : ℂ) ^ (-s : ℂ) = 1 := by
    rw [integral_Ioi_cpow_of_lt (by rwa [neg_re, neg_lt_neg_iff]) zero_lt_one, ofReal_one,
      one_cpow, show -(s : ℂ) + 1 = -(s - 1) by ring, neg_div_neg_eq, mul_div_cancel₀]
    exact (sub_ne_zero.trans ofReal_ne_one).mpr hs.ne'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
h₃ :
  (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1
Cs : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
⊢ Cs ≤ C

Tactic:
setIntegral_mono_on ?_ h₂ measurableSet_Ioc fun t ht ↦ ?_

Premises used: measurableSet_Ioc, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
h₃ :
  (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1
Cs : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
refine_1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioc 1 T) volume
refine_2 :
  ∀ (t : ℝ) (ht : t ∈ Set.Ioc 1 T),
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
⊢ Cs ≤ C

Tactic:
refine setIntegral_mono_on ?_ h₂ measurableSet_Ioc fun t ht ↦ ?_

Premises used: measurableSet_Ioc, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
h₃ :
  (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1
Cs : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioc 1 T) volume

Tactic:
h₁.mono_set <| Set.Ioc_subset_Ioi_self.trans Set.Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, HasSubset.Subset.trans, Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
h₃ :
  (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1
Cs : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioc 1 T) volume

Tactic:
exact h₁.mono_set <| Set.Ioc_subset_Ioi_self.trans Set.Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, HasSubset.Subset.trans, Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set