awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
h_bound :
  ∀ (hs : 1 ≤ s),
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
      ‖(a - (↑(n + 1) : ℝ)) / a ^ (s + 1)‖ ≤ (a - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) a 2
⊢ Membership.mem («γ» := Set ℝ) (Ici 1) s →
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
      ‖(a - (↑(n + 1) : ℝ)) / a ^ (s + 1)‖ ≤ (a - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) a 2

Tactic:
(hs : 1 ≤ s)
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
h_bound :
  ∀ᵐ (x : ℝ),
    x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) →
      ‖(x - (↑(n + 1) : ℝ)) / x ^ (s + 1)‖ ≤ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
    ‖(a - (↑(n + 1) : ℝ)) / a ^ (s + 1)‖ ≤ (a - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) a 2

Tactic:
rw [ae_restrict_iff' measurableSet_Ioc]

Premises used: MeasureTheory.ae_restrict_iff', measurableSet_Ioc
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
h_bound :
  ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
    ‖(x - (↑(n + 1) : ℝ)) / x ^ (s + 1)‖ ≤ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) →
      ‖(x - (↑(n + 1) : ℝ)) / x ^ (s + 1)‖ ≤ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2

Tactic:
filter_upwards with x hx
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ LE.le (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ 1 < x

Tactic:
have : 1 < x := lt_of_le_of_lt (by simp) hx.1
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
⊢ 0 ≤ x ^ (s + 1)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
h_bound :
  (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / x ^ (s + 1) ≤ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / HPow.hPow (β := ℝ) x 2
⊢ ‖(x - (↑(n + 1) : ℝ)) / x ^ (s + 1)‖ ≤ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2

Tactic:
rw [norm_of_nonneg (div_nonneg (sub_nonneg.mpr hx.1.le) (by positivity)), Nat.cast_add_one]

Premises used: Iff.mpr, LT.lt.le, And.left, div_nonneg, Nat.cast_add_one, sub_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
h_bound : 0 ≤ x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_bound₁ : 1 ≤ x
h_bound₂ : 2 ≤ s + 1
⊢ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / x ^ (s + 1) ≤ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / HPow.hPow (β := ℝ) x 2

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
⊢ 0 ≤ x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
exact_mod_cast sub_nonneg.mpr hx.1.le

Premises used: Iff.mpr, LT.lt.le, And.left, sub_nonneg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
⊢ 1 ≤ x

Tactic:
this.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
⊢ 1 ≤ x

Tactic:
exact this.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
linarith : s + 1 < 2 → 1 - s + (s + 1 - 2) = 0
⊢ 2 ≤ s + 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
bound_integrable :
  IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2) volume (↑(n + 1) : ℝ)
    (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2)
    (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)))

Tactic:
rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith)]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le, MeasureTheory.IntegrableOn
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
⊢ 0 < n + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2) volume (↑(n + 1) : ℝ)
    (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)

Tactic:
exact_mod_cast term_welldef (by lia : 0 < (n + 1)) zero_lt_one

Premises used: zero_lt_one, ZetaAsymptotics.term_welldef
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
h_cont :
  ∀ᵐ (x : ℝ),
    x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) →
      ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
    ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (a - (↑(n + 1) : ℝ)) / a ^ (x + 1)) (Ici 1)

Tactic:
rw [ae_restrict_iff' measurableSet_Ioc]

Premises used: MeasureTheory.ae_restrict_iff', measurableSet_Ioc
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
h_cont :
  ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
    ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) →
      ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)

Tactic:
filter_upwards with x hx
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)

Tactic:
continuousOn_of_forall_continuousAt (fun s (hs : 1 ≤ s) ↦ continuousAt_const.div ?_ ?_)

Premises used: continuousOn_of_forall_continuousAt, continuousAt_const, ContinuousAt.div
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
h_cont : ∀ (s : ℝ) (hs : 1 ≤ s), ContinuousAt (Y := ℝ) (fun (x_1 : ℝ) ↦ x ^ (x_1 + 1)) s
h_cont₁ : ∀ (s : ℝ) (hs : 1 ≤ s), x ^ (s + 1) ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)

Tactic:
refine continuousOn_of_forall_continuousAt (fun s (hs : 1 ≤ s) ↦ continuousAt_const.div ?_ ?_)

Premises used: continuousOn_of_forall_continuousAt, continuousAt_const, ContinuousAt.div
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
s : ℝ
hs : 1 ≤ s
linarith : s + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - s) + (s + 1 - 0) = 0
linarith₁ : s + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < s + 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
s : ℝ
hs : 1 ≤ s
⊢ ContinuousAt (Y := ℝ) (fun (x_1 : ℝ) ↦ x ^ (x_1 + 1)) s

Tactic:
exact continuousAt_const.rpow (continuousAt_id.add continuousAt_const) (Or.inr (by linarith))

Premises used: ContinuousAt.add, continuousAt_const, ContinuousAt.rpow, continuousAt_id, Or.inr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
s : ℝ
hs : 1 ≤ s
⊢ 0 < n + 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
s : ℝ
hs : 1 ≤ s
⊢ x ^ (s + 1) ≠ 0

Tactic:
exact (rpow_pos_of_pos ((Nat.cast_pos.mpr (by simp)).trans hx.1) _).ne'

Premises used: Iff.mpr, Real.rpow_pos_of_pos, Nat.cast_pos, LT.lt.ne', And.left, LT.lt.trans
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ ContinuousOn term_tsum (Ici 1)

Tactic:
continuousOn_tsum (fun i ↦ continuousOn_term _) term_tsum_one.summable (fun n s hs ↦ ?_)

Premises used: continuousOn_tsum, ZetaAsymptotics.term_tsum, ZetaAsymptotics.continuousOn_term, ZetaAsymptotics.term_tsum_one, HasSum.summable
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
refine : ∀ (n : ℕ) (s : ℝ) (hs : Membership.mem («γ» := Set ℝ) (Ici 1) s), ‖term (n + 1) s‖ ≤ term (n + 1) 1
⊢ ContinuousOn term_tsum (Ici 1)

Tactic:
refine continuousOn_tsum (fun i ↦ continuousOn_term _) term_tsum_one.summable (fun n s hs ↦ ?_)

Premises used: continuousOn_tsum, ZetaAsymptotics.continuousOn_term, ZetaAsymptotics.term_tsum_one, HasSum.summable
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
rw :
  LE.le (α := ℝ) (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1,
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
rw₁ :
  LE.le (α := ℝ) 0
    (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
⊢ ‖term (n + 1) s‖ ≤ term (n + 1) 1

Tactic:
rw [term, term, norm_of_nonneg]

Premises used: ZetaAsymptotics.term, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
linarith :
  HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 < (↑(n + 1) : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 - (↑(n + 1) : ℝ)) = 0
⊢ (↑(n + 1) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
simp_rw :
  LE.le (α := ℝ)
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1,
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)

Tactic:
simp_rw [intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)]

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)

Tactic:
setIntegral_mono_on ?_ ?_ measurableSet_Ioc (fun x hx ↦ ?_)

Premises used: measurableSet_Ioc, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
refine_1 :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume
refine_2 :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
    (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume
refine_3 :
  ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
    (x - (↑(n + 1) : ℝ)) / x ^ (s + 1) ≤ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)

Tactic:
refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc (fun x hx ↦ ?_)

Premises used: measurableSet_Ioc, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume

Tactic:
(term_welldef n.succ_pos (zero_lt_one.trans_le hs)).1

Premises used: zero_lt_one, And.left, LT.lt.trans_le, Nat.succ_pos, ZetaAsymptotics.term_welldef
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume

Tactic:
exact (term_welldef n.succ_pos (zero_lt_one.trans_le hs)).1

Premises used: zero_lt_one, And.left, LT.lt.trans_le, Nat.succ_pos, ZetaAsymptotics.term_welldef
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
    (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume

Tactic:
(term_welldef n.succ_pos zero_lt_one).1

Premises used: zero_lt_one, And.left, Nat.succ_pos, ZetaAsymptotics.term_welldef
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
    (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume

Tactic:
exact (term_welldef n.succ_pos zero_lt_one).1

Premises used: zero_lt_one, And.left, Nat.succ_pos, ZetaAsymptotics.term_welldef
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ LE.le (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ 1 ≤ x

Tactic:
have : 1 ≤ x := le_trans (by simp) hx.1.le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 ≤ x
refine_3 : 0 ≤ x - (↑(n + 1) : ℝ)
refine_3₁ : 1 ≤ s
⊢ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1) ≤ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 ≤ x
⊢ 0 ≤ x - (↑(n + 1) : ℝ)

Tactic:
sub_nonneg.mpr hx.1.le

Premises used: Iff.mpr, LT.lt.le, And.left, sub_nonneg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 ≤ x
⊢ 0 ≤ x - (↑(n + 1) : ℝ)

Tactic:
exact sub_nonneg.mpr hx.1.le

Premises used: Iff.mpr, LT.lt.le, And.left, sub_nonneg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 ≤ x
⊢ 1 ≤ s

Tactic:
hs

Premises used: Set.Ici, Set.Mem
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 ≤ x
⊢ 1 ≤ s

Tactic:
exact hs
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
rw :
  LE.le (α := ℝ) 0
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
⊢ LE.le (α := ℝ) 0
    (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))

Tactic:
rw [intervalIntegral.integral_of_le (by linarith)]

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))

Tactic:
setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ div_nonneg ?_ (rpow_nonneg ?_ _))

Premises used: HAdd.hAdd, MeasureTheory.setIntegral_nonneg, div_nonneg, Real.rpow_nonneg, measurableSet_Ioc, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
refine_1 : ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)), 0 ≤ x - (↑(n + 1) : ℝ)
refine_2 : ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)), 0 ≤ x
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))

Tactic:
refine setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ div_nonneg ?_ (rpow_nonneg ?_ _))

Premises used: MeasureTheory.setIntegral_nonneg, div_nonneg, Real.rpow_nonneg, measurableSet_Ioc
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
linarith : x - (↑(n + 1) : ℝ) < 0 → x - (↑(n + 1) : ℝ) - 0 + ((↑(n + 1) : ℝ) - x) = 0
⊢ 0 ≤ x - (↑(n + 1) : ℝ)

Tactic:
linarith [hx.1]

Premises used: And.left
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
linarith : x < 0 → HSub.hSub (α := ℝ) 0 (↑(n + 1) : ℝ) + (x - 0) + ((↑(n + 1) : ℝ) - x) = 0
⊢ 0 ≤ x

Tactic:
linarith [hx.1]

Premises used: And.left
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
apply :
  (Complex.ofReal ∘ fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) =ᶠ[𝓝[>] 1]
    fun (s : ℝ) ↦ riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)
⊢ Tendsto (fun (s : ℝ) ↦ riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)) (𝓝[>] 1) (𝓝 (↑γ : ℂ))

Tactic:
apply ((Complex.continuous_ofReal.tendsto _).comp this).congr'

Premises used: Continuous.tendsto, Real.eulerMascheroniConstant, Complex.continuous_ofReal, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
h :
  ∀ (s : ℝ) (hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s),
    (Complex.ofReal ∘ fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) s =
      riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)
⊢ (Complex.ofReal ∘ fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) =ᶠ[𝓝[>] 1]
    fun (s : ℝ) ↦ riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)

Tactic:
filter_upwards [self_mem_nhdsWithin] with s hs

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
h : ∑' (a : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ s) : ℂ) = riemannZeta (↑s : ℂ)
⊢ (Complex.ofReal ∘ fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) s =
    riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)

Tactic:
simp only [Function.comp_apply, Complex.ofReal_sub, Complex.ofReal_div,
      Complex.ofReal_one, sub_left_inj, Complex.ofReal_tsum]

Premises used: Complex.ofReal_one, sub_left_inj, Complex.ofReal_div, Complex.ofReal_sub, Function.comp_apply, Complex.ofReal_tsum
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
⊢ 1 < (↑s : ℂ).re

Tactic:
simpa using hs
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
h :
  Eq (α := ℂ) (∑' (a : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ s) : ℂ))
    (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ))
⊢ ∑' (a : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ s) : ℂ) = riemannZeta (↑s : ℂ)

Tactic:
rw [zeta_eq_tsum_one_div_nat_add_one_cpow (by simpa using hs)]

Premises used: zeta_eq_tsum_one_div_nat_add_one_cpow
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
h : ∀ (n : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) : ℂ) = 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ)
⊢ Eq (α := ℂ) (∑' (a : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ s) : ℂ))
    (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ))

Tactic:
congr 1 with n
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
n : ℕ
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
n : ℕ
h : 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑s : ℂ) = 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ)
⊢ 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) : ℂ) = 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ)

Tactic:
rw [Complex.ofReal_cpow (by positivity)]

Premises used: Complex.ofReal_cpow
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
n : ℕ
h h₁ h₂ h₃ : 1 / HPow.hPow (α := ℂ) (↑(n + 1) : ℂ) (↑s : ℂ) = 1 / HPow.hPow (α := ℂ) (↑(n + 1) : ℂ) (↑s : ℂ)
⊢ 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑s : ℂ) = 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
suffices : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
⊢ Tendsto (fun (s : ℝ) ↦ riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)) (𝓝[>] 1) (𝓝 (↑γ : ℂ))

Tactic:
suffices Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1))
    (𝓝[>] 1) (𝓝 γ) by
    apply ((Complex.continuous_ofReal.tendsto _).comp this).congr'
    filter_upwards [self_mem_nhdsWithin] with s hs
    simp only [Function.comp_apply, Complex.ofReal_sub, Complex.ofReal_div,
      Complex.ofReal_one, sub_left_inj, Complex.ofReal_tsum]
    rw [zeta_eq_tsum_one_div_nat_add_one_cpow (by simpa using hs)]
    congr 1 with n
    rw [Complex.ofReal_cpow (by positivity)]
    norm_cast