-- Mathlib/NumberTheory/LSeries/Convergence.lean
/-- If `f` is real-valued and `x` is strictly greater than the abscissa of absolute convergence
of `f`, then the real series `∑' n, f n / n ^ x` converges. -/
lemma LSeries.summable_real_of_abscissaOfAbsConv_lt {f : ℕ → ℝ} {x : ℝ}
    (h : abscissaOfAbsConv (f ·) < x) :
    Summable fun n : ℕ ↦ f n / (n : ℝ) ^ x

Proof state:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
aux : term (fun x => ↑(f x)) ↑x = fun n => ↑(if n = 0 then 0 else f n / ↑n ^ x)
⊢ Summable fun n => f n / ↑n ^ x

Tactic:
have := LSeriesSummable_of_abscissaOfAbsConv_lt_re (ofReal_re x ▸ h)

Result:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
aux : term (fun x => ↑(f x)) ↑x = fun n => ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : LSeriesSummable (fun x => ↑(f x)) ↑x
⊢ Summable fun n => f n / ↑n ^ x

Proof state:
case h
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
n : ℕ
⊢ term (fun x => ↑(f x)) (↑x) n = ↑(if n = 0 then 0 else f n / ↑n ^ x)

Tactic:
simp [term_def, apply_ite ((↑) : ℝ → ℂ), ofReal_cpow n.cast_nonneg]

Result:
no goals

Proof state:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
aux : term (fun x => ↑(f x)) ↑x = fun n => ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : Summable fun x_1 => if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x
⊢ (fun x_1 => if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x) =ᶠ[Filter.cofinite] fun n => f n / ↑n ^ x

Tactic:
filter_upwards [(Set.finite_singleton 0).compl_mem_cofinite] with n hn
  using if_neg (by simpa using hn)

Result:
no goals

Proof state:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
aux : term (fun x => ↑(f x)) ↑x = fun n => ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : Summable fun x_1 => if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x
n : ℕ
hn : n ∈ {0}ᶜ
⊢ ¬n = 0

Tactic:
simpa using hn

Result:
no goals

Proof state:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
aux : term (fun x => ↑(f x)) ↑x = fun n => ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : Summable fun x_1 => if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x
⊢ Summable fun n => f n / ↑n ^ x

Tactic:
refine this.congr_cofinite ?_

Result:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
aux : term (fun x => ↑(f x)) ↑x = fun n => ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : Summable fun x_1 => if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x
⊢ (fun x_1 => if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x) =ᶠ[Filter.cofinite] fun n => f n / ↑n ^ x

Proof state:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
aux : term (fun x => ↑(f x)) ↑x = fun n => ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : LSeriesSummable (fun x => ↑(f x)) ↑x
⊢ Summable fun n => f n / ↑n ^ x

Tactic:
simp only [LSeriesSummable, aux, summable_ofReal] at this

Result:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
aux : term (fun x => ↑(f x)) ↑x = fun n => ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : Summable fun x_1 => if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x
⊢ Summable fun n => f n / ↑n ^ x

Proof state:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
⊢ term (fun x => ↑(f x)) ↑x = fun n => ↑(if n = 0 then 0 else f n / ↑n ^ x)

Tactic:
ext n

Result:
case h
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x => ↑(f x)) < ↑x
n : ℕ
⊢ term (fun x => ↑(f x)) (↑x) n = ↑(if n = 0 then 0 else f n / ↑n ^ x)