Theorem: LSeries.eq_of_LSeries_eventually_eq (EulerProducts/LSeriesUnique.lean)

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
⊢ f n = g n
Tactic:
have hsub : (fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ) :=
  LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq hf hg h
State after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
⊢ f n = g n

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
⊢ f n = g n
Tactic:
have ha : abscissaOfAbsConv (f - g) ≠ ⊤ :=
  lt_top_iff_ne_top.mp <| (abscissaOfAbsConv_sub_le f g).trans_lt <| max_lt hf hg
State after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
ha : abscissaOfAbsConv (f - g) ≠ ⊤
⊢ f n = g n

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
n : ℕ
hn : n ≠ 0
hsub : (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
ha : abscissaOfAbsConv (f - g) ≠ ⊤
⊢ f n = g n
Tactic:
simpa only [Pi.sub_apply, sub_eq_zero]
  using (LSeries_eventually_eq_zero_iff'.mp hsub).resolve_right ha n hn
State after:
no goals