Theorem: LSeries_eq_iff_of_abscissaOfAbsConv_lt_top (EulerProducts/LSeriesUnique.lean)

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ f n = g n
Tactic:
refine eq_of_LSeries_eventually_eq hf hg ?_ hn
State after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x
Tactic:
exact Filter.eventually_of_forall fun x ↦ congr_fun H x
State after:
no goals