-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- If the L-series of `f` converges at some point, then `f 1` is the limit of `LSeries f x`
as `x → ∞`. -/
lemma LSeries.tendsto_atTop {f : ℕ → ℂ} (ha : abscissaOfAbsConv f < ⊤):
    Tendsto (fun x : ℝ ↦ LSeries f x) atTop (nhds (f 1))

Proof state:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

Tactic:
have ha' : abscissaOfAbsConv F < ⊤ := (abscissaOfAbsConv_congr hF).symm ▸ ha

Result:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

Proof state:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

Tactic:
let F (n : ℕ) : ℂ := if n = 0 then 0 else f n

Result:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

Proof state:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

Tactic:
have hF₀ : F 0 = 0 := rfl

Result:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

Proof state:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun x => LSeries F ↑x) atTop (nhds (f 1))

Tactic:
convert LSeries.tendsto_cpow_mul_atTop (n := 0) (fun _ hm ↦ Nat.le_zero.mp hm ▸ hF₀) ha' using 1

Result:
case h.e'_3
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ (fun x => LSeries F ↑x) = fun x => (↑0 + 1) ^ ↑x * LSeries F ↑x

Proof state:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

Tactic:
simp_rw [← LSeries_congr _ hF]

Result:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun x => LSeries F ↑x) atTop (nhds (f 1))

Proof state:
case h.e'_3
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ (fun x => LSeries F ↑x) = fun x => (↑0 + 1) ^ ↑x * LSeries F ↑x

Tactic:
simp

Result:
no goals

Proof state:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

Tactic:
have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn

Result:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))