-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma continuousOn_term_tsum : ContinuousOn term_tsum (Ici 1)

Proof state:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 1 ≤ ↑(n + 1)

Tactic:
simp

Result:
no goals

Proof state:
case refine_3.hyz
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 1 + 1 ≤ s + 1

Tactic:
linarith [mem_Ici.mp hs]

Result:
no goals

Proof state:
case refine_3.hb
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 < x ^ (s + 1)

case refine_3.hc
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 < x ^ (1 + 1)

Tactic:
all_goals apply rpow_pos_of_pos ((Nat.cast_nonneg _).trans_lt hx.1)

Result:
no goals

Proof state:
case refine_3.ha
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 < x - ↑(n + 1)

Tactic:
linarith [hx.1]

Result:
no goals

Proof state:
case refine_3
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ x ^ (1 + 1) ≤ x ^ (s + 1)

Tactic:
apply rpow_le_rpow_of_exponent_le

Result:
case refine_3.hx
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 1 ≤ x

case refine_3.hyz
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 1 + 1 ≤ s + 1

Proof state:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ‖term (n + 1) s‖ ≤ term (n + 1) 1

Tactic:
rw [term, term, norm_of_nonneg]

Result:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1) ≤
    ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (1 + 1)

n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ 0 ≤ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1)

Proof state:
case refine_1
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 ≤ x - ↑(n + 1)

case refine_2
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 ≤ x

Tactic:
all_goals linarith [hx.1]

Result:
no goals

Proof state:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1) ≤
    ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (1 + 1)

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

Result:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ∫ (x : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x - ↑(n + 1)) / x ^ (s + 1) ∂volume ≤
    ∫ (x : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x - ↑(n + 1)) / x ^ (1 + 1) ∂volume

Proof state:
case refine_3.hc
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 < x ^ (1 + 1)

Tactic:
apply rpow_pos_of_pos ((Nat.cast_nonneg _).trans_lt hx.1)

Result:
no goals

Proof state:
case refine_3
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ (x - ↑(n + 1)) / x ^ (s + 1) ≤ (x - ↑(n + 1)) / x ^ (1 + 1)

Tactic:
rw [div_le_div_iff_of_pos_left]

Result:
case refine_3
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ x ^ (1 + 1) ≤ x ^ (s + 1)

case refine_3.ha
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 < x - ↑(n + 1)

case refine_3.hb
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 < x ^ (s + 1)

case refine_3.hc
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 < x ^ (1 + 1)

Proof state:
⊢ ContinuousOn term_tsum (Ici 1)

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

Result:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ‖term (n + 1) s‖ ≤ term (n + 1) 1

Proof state:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ 0 ≤ ∫ (x : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x - ↑(n + 1)) / x ^ (s + 1) ∂volume

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

Result:
case refine_1
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 ≤ x - ↑(n + 1)

case refine_2
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 ≤ x

Proof state:
case refine_2
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 ≤ x

Tactic:
linarith [hx.1]

Result:
no goals

Proof state:
case refine_3.hx
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 1 ≤ x

Tactic:
exact (lt_of_le_of_lt (by simp) hx.1).le

Result:
no goals

Proof state:
case refine_1
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ IntegrableOn (fun x => (x - ↑(n + 1)) / x ^ (s + 1)) (Ioc (↑(n + 1)) (↑(n + 1) + 1)) volume

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

Result:
no goals

Proof state:
case refine_2
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ IntegrableOn (fun x => (x - ↑(n + 1)) / x ^ (1 + 1)) (Ioc (↑(n + 1)) (↑(n + 1) + 1)) volume

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

Result:
no goals

Proof state:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ 0 ≤ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1)

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

Result:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ 0 ≤ ∫ (x : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x - ↑(n + 1)) / x ^ (s + 1) ∂volume

Proof state:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ↑(n + 1) ≤ ↑(n + 1) + 1

Tactic:
linarith

Result:
no goals

Proof state:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ∫ (x : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x - ↑(n + 1)) / x ^ (s + 1) ∂volume ≤
    ∫ (x : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x - ↑(n + 1)) / x ^ (1 + 1) ∂volume

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

Result:
case refine_1
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ IntegrableOn (fun x => (x - ↑(n + 1)) / x ^ (s + 1)) (Ioc (↑(n + 1)) (↑(n + 1) + 1)) volume

case refine_2
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ IntegrableOn (fun x => (x - ↑(n + 1)) / x ^ (1 + 1)) (Ioc (↑(n + 1)) (↑(n + 1) + 1)) volume

case refine_3
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ (x - ↑(n + 1)) / x ^ (s + 1) ≤ (x - ↑(n + 1)) / x ^ (1 + 1)