-- Mathlib/Analysis/PSeries.lean
lemma Real.summable_one_div_nat_add_rpow (a : ℝ) (s : ℝ) :
    Summable (fun n : ℕ ↦ 1 / |n + a| ^ s) ↔ 1 < s

Proof state:
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this✝ : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)
⊢ 1 ≠ 0 ∨ 0 ≤ s

Tactic:
simp

Result:
no goals

Proof state:
a s : ℝ
⊢ (Summable fun n => 1 / |↑n + a| ^ s) ↔ 1 < s

Tactic:
suffices ∀ (b c : ℝ), Summable (fun n : ℕ ↦ 1 / |n + b| ^ s) →
    Summable (fun n : ℕ ↦ 1 / |n + c| ^ s) by
  simp_rw [← summable_one_div_nat_rpow, Iff.intro (this a 0) (this 0 a), add_zero, Nat.abs_cast]

Result:
a s : ℝ
⊢ ∀ (b c : ℝ), (Summable fun n => 1 / |↑n + b| ^ s) → Summable fun n => 1 / |↑n + c| ^ s

Proof state:
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
⊢ Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)

Tactic:
refine (this.comp (tendsto_id.atTop_add (tendsto_const_nhds (x := c)))).congr' ?_

Result:
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
⊢ ((fun x => 1 + (b - c) / x) ∘ fun x => id x + c) =ᶠ[atTop] fun x => (x + b) / (x + c)

Proof state:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |↑n + b| ^ s = 0
⊢ 1 / |↑n + c| ^ s = 0

Tactic:
have hna : 0 < n + b := by linarith [lt_of_abs_lt ((abs_neg b).symm ▸ Nat.lt_of_ceil_lt hn)]

Result:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |↑n + b| ^ s = 0
hna : 0 < ↑n + b
⊢ 1 / |↑n + c| ^ s = 0

Proof state:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hna : 0 < ↑n + b
⊢ 1 / |↑n + b| ^ s = 0 → False

Tactic:
positivity

Result:
no goals

Proof state:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
x : ℝ
hx : -c < x
⊢ ((fun x => 1 + (b - c) / x) ∘ fun x => id x + c) x = (x + b) / (x + c)

Tactic:
field_simp [(by linarith : 0 < x + c).ne']

Result:
no goals

Proof state:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this✝ : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)
⊢ Tendsto (fun x => |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)

Tactic:
apply (one_rpow s ▸ (continuousAt_rpow_const _ s (by simp)).tendsto.comp this).congr'

Result:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this✝ : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)
⊢ ((fun x => x ^ s) ∘ fun x => (x + b) / (x + c)) =ᶠ[atTop] fun x => |x + b| ^ s / |x + c| ^ s

Proof state:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |↑n + b| ^ s = 0
hna : 0 < ↑n + b
⊢ False

Tactic:
revert hx

Result:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hna : 0 < ↑n + b
⊢ 1 / |↑n + b| ^ s = 0 → False

Proof state:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this✝ : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)
⊢ ((fun x => x ^ s) ∘ fun x => (x + b) / (x + c)) =ᶠ[atTop] fun x => |x + b| ^ s / |x + c| ^ s

Tactic:
filter_upwards [eventually_gt_atTop (-b), eventually_gt_atTop (-c)] with x hb hc

Result:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this✝ : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : -b < x
hc : -c < x
⊢ ((fun x => x ^ s) ∘ fun x => (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s

Proof state:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
⊢ Tendsto ((fun n => 1 / |↑n + c| ^ s) / fun n => 1 / |↑n + b| ^ s) atTop (𝓝 1)

Tactic:
simp_rw [Pi.div_def, div_div, mul_one_div, one_div_div]

Result:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
⊢ Tendsto (fun i => |↑i + b| ^ s / |↑i + c| ^ s) atTop (𝓝 1)

Proof state:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this✝ : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : 0 < x + b
hc : 0 < x + c
⊢ ((fun x => x ^ s) ∘ fun x => (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s

Tactic:
rw [Function.comp_apply, div_rpow hb.le hc.le, abs_of_pos hb, abs_of_pos hc]

Result:
no goals

Proof state:
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
x : ℝ
hx : -c < x
⊢ 0 < x + c

Tactic:
linarith

Result:
no goals

Proof state:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this✝ : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : -b < x
hc : -c < x
⊢ ((fun x => x ^ s) ∘ fun x => (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s

Tactic:
rw [neg_lt_iff_pos_add] at hb hc

Result:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this✝ : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : 0 < x + b
hc : 0 < x + c
⊢ ((fun x => x ^ s) ∘ fun x => (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s

Proof state:
case refine_1
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
⊢ ∀ᶠ (x : ℕ) in atTop, 1 / |↑x + b| ^ s = 0 → 1 / |↑x + c| ^ s = 0

Tactic:
filter_upwards [eventually_gt_atTop (Nat.ceil |b|)] with n hn hx

Result:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |↑n + b| ^ s = 0
⊢ 1 / |↑n + c| ^ s = 0

Proof state:
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |↑n + b| ^ s = 0
⊢ 0 < ↑n + b

Tactic:
linarith [lt_of_abs_lt ((abs_neg b).symm ▸ Nat.lt_of_ceil_lt hn)]

Result:
no goals

Proof state:
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
⊢ Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)

Tactic:
simpa using tendsto_const_nhds.add ((tendsto_const_nhds (X := ℝ)).div_atTop tendsto_id)

Result:
no goals

Proof state:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
⊢ Tendsto (fun x => |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)

Tactic:
have : Tendsto (fun x ↦ (x + b) / (x + c)) atTop (𝓝 1) := by
  refine (this.comp (tendsto_id.atTop_add (tendsto_const_nhds (x := c)))).congr' ?_
  filter_upwards [eventually_gt_atTop (-c)] with x hx
  field_simp [(by linarith : 0 < x + c).ne']

Result:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this✝ : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (fun x => (x + b) / (x + c)) atTop (𝓝 1)
⊢ Tendsto (fun x => |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)

Proof state:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
⊢ Tendsto (fun x => |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)

Tactic:
have : Tendsto (fun x : ℝ ↦ 1 + (b - c) / x) atTop (𝓝 1) := by
  simpa using tendsto_const_nhds.add ((tendsto_const_nhds (X := ℝ)).div_atTop tendsto_id)

Result:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
⊢ Tendsto (fun x => |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)

Proof state:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |↑n + b| ^ s = 0
hna : 0 < ↑n + b
⊢ 1 / |↑n + c| ^ s = 0

Tactic:
exfalso

Result:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |↑n + b| ^ s = 0
hna : 0 < ↑n + b
⊢ False