-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- The `LSeries` of `f` is zero for large real arguments if and only if either `f n = 0`
for all `n ≠ 0` or the L-series converges nowhere. -/
lemma LSeries_eventually_eq_zero_iff' {f : ℕ → ℂ} :
    (fun x : ℝ ↦ LSeries f x) =ᶠ[atTop] 0 ↔ (∀ n ≠ 0, f n = 0) ∨ abscissaOfAbsConv f = ⊤

Proof state:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
ih : ∀ m < n, F m = 0
this : Tendsto (fun x => ↑n ^ ↑x * LSeries F ↑x) atTop (nhds (F n))
⊢ F n = 0

Tactic:
replace this := this.congr' <| H' n

Result:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
ih : ∀ m < n, F m = 0
this : Tendsto (fun x => 0) atTop (nhds (F n))
⊢ F n = 0

Proof state:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
⊢ ∀ (n : ℕ), F n = 0

Tactic:
intro n

Result:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
⊢ F n = 0

Proof state:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

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

Result:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

Proof state:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0

Tactic:
simp only [h']

Result:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ (fun x => ↑n ^ ↑x * LSeries f ↑x) =ᶠ[atTop] fun x => 0

Proof state:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

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

Result:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

Proof state:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
ih : ∀ m < n, F m = 0
this : 0 = F n
⊢ F n = 0

Tactic:
exact this.symm

Result:
no goals

Proof state:
case pos
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0

Tactic:
exact Eventually.of_forall <| by simp [LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h]

Result:
no goals

Proof state:
f : ℕ → ℂ
h : ¬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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
s : Set ℝ
hs : s ∈ atTop ∧ Set.EqOn (fun x => LSeries f ↑x) 0 s
x : ℝ
hx : x ∈ s
⊢ (fun x => ↑n ^ ↑x * LSeries f ↑x) x = (fun x => 0) x

Tactic:
simp [hs.2 hx]

Result:
no goals

Proof state:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
ih : ∀ m < n, F m = 0
this : Tendsto (fun x => 0) atTop (nhds (F n))
⊢ F n = 0

Tactic:
simp only [tendsto_const_nhds_iff] at this

Result:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
ih : ∀ m < n, F m = 0
this : 0 = F n
⊢ F n = 0

Proof state:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ ∀ (n : ℕ), F n = 0

Tactic:
have ha : ¬ abscissaOfAbsConv F = ⊤ := abscissaOfAbsConv_congr hF ▸ h

Result:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
⊢ ∀ (n : ℕ), F n = 0

Proof state:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∃ s ∈ atTop, Set.EqOn (fun x => LSeries f ↑x) 0 s
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ ∃ s ∈ atTop, Set.EqOn (fun x => ↑n ^ ↑x * LSeries f ↑x) (fun x => 0) s

Tactic:
obtain ⟨s, hs⟩ := H

Result:
case intro
f : ℕ → ℂ
h : ¬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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
s : Set ℝ
hs : s ∈ atTop ∧ Set.EqOn (fun x => LSeries f ↑x) 0 s
⊢ ∃ s ∈ atTop, Set.EqOn (fun x => ↑n ^ ↑x * LSeries f ↑x) (fun x => 0) s

Proof state:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
⊢ ∀ (n : ℕ), F n = 0

Tactic:
have H' (n : ℕ) : (fun x : ℝ ↦ n ^ (x : ℂ) * LSeries F x) =ᶠ[atTop] fun _ ↦ 0 := by
  simp only [h']
  rw [eventuallyEq_iff_exists_mem] at H ⊢
  obtain ⟨s, hs⟩ := H
  exact ⟨s, hs.1, fun x hx ↦ by simp [hs.2 hx]⟩

Result:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
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 = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
⊢ ∀ (n : ℕ), F n = 0