Theorem: LSeries_eventually_eq_zero_iff' (EulerProducts/LSeriesUnique.lean)

State before:
f : ℕ → ℂ
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0 ↔ (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤
Tactic:
by_cases h : abscissaOfAbsConv f = ⊤ <;> simp only [h, or_true, or_false, iff_true]
State after:
case pos
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0

case neg
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0

State before:
case pos
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0
Tactic:
refine eventually_of_forall ?_
State after:
case pos
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ ∀ (x : ℝ), (fun x => LSeries f ↑x) x = 0 x

State before:
case pos
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ ∀ (x : ℝ), (fun x => LSeries f ↑x) x = 0 x
Tactic:
simp only [LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h, Pi.zero_apply, forall_const]
State after:
no goals

State before:
case neg
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0
Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ eventually_of_forall fun x ↦ ?_⟩
State after:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
⊢ ∀ (n : ℕ), n ≠ 0 → f n = 0

case neg.refine_2
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∀ (n : ℕ), n ≠ 0 → f n = 0
x : ℝ
⊢ (fun x => LSeries f ↑x) x = 0 x

State before:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
⊢ ∀ (n : ℕ), n ≠ 0 → f n = 0
Tactic:
let F (n : ℕ) : ℂ := if n = 0 then 0 else f n
State after:
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

State before:
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
State after:
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

State before:
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 := by simp only [hn, ↓reduceIte, F]
State after:
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

State before:
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
Tactic:
suffices ∀ n, F n = 0 by
  peel hF with n hn h
  exact (this n ▸ h).symm
State after:
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

State before:
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
State after:
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

State before:
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
Tactic:
have h' (x : ℝ) : LSeries F x = LSeries f x := LSeries_congr x hF
State after:
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

State before:
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 ⊢
  peel H with s hs
  refine ⟨hs.1, fun x hx ↦ ?_⟩
  simp only [hs.2 hx, Pi.zero_apply, mul_zero]
State after:
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

State before:
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
State after:
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

State before:
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:
induction' n using Nat.strongInductionOn with n ih
State after:
case neg.refine_1.ind
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
⊢ F n = 0

State before:
case neg.refine_1.ind
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
⊢ F n = 0
Tactic:
suffices Tendsto (fun x : ℝ ↦ (n ^ (x : ℂ)) * LSeries F x) atTop (nhds (F n)) by
  replace this := this.congr' <| H' n
  simp only [tendsto_const_nhds_iff] at this
  exact this.symm
State after:
case neg.refine_1.ind
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
⊢ Tendsto (fun x => ↑n ^ ↑x * LSeries F ↑x) atTop (nhds (F n))

State before:
case neg.refine_1.ind
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
⊢ Tendsto (fun x => ↑n ^ ↑x * LSeries F ↑x) atTop (nhds (F n))
Tactic:
cases n with
| zero =>
    refine Tendsto.congr' (H' 0).symm ?_
    simp only [zero_eq, hF₀, tendsto_const_nhds_iff]
| succ n =>
    simp only [succ_eq_add_one, cast_add, cast_one]
    exact LSeries.tendsto_pow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <| Ne.lt_top ha
State after:
no goals

State before:
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 : ℕ
hn : n ≠ 0
⊢ F n = f n
Tactic:
simp only [hn, ↓reduceIte, F]
State after:
no goals

State before:
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
this : ∀ (n : ℕ), F n = 0
⊢ ∀ (n : ℕ), n ≠ 0 → f n = 0
Tactic:
peel hF with n hn h
State after:
case h.h
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
this : ∀ (n : ℕ), F n = 0
n : ℕ
hn : n ≠ 0
h : F n = f n
⊢ f n = 0

State before:
case h.h
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
this : ∀ (n : ℕ), F n = 0
n : ℕ
hn : n ≠ 0
h : F n = f n
⊢ f n = 0
Tactic:
exact (this n ▸ h).symm
State after:
no goals

State before:
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']
State after:
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

State before:
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:
rw [eventuallyEq_iff_exists_mem] at H ⊢
State after:
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

State before:
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:
peel H with s hs
State after:
case h
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 : 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

State before:
case h
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 : 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
Tactic:
refine ⟨hs.1, fun x hx ↦ ?_⟩
State after:
case h
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 : 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

State before:
case h
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 : 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 only [hs.2 hx, Pi.zero_apply, mul_zero]
State after:
no goals

State before:
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
State after:
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

State before:
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
State after:
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

State before:
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
State after:
no goals

State before:
case neg.refine_1.ind.zero
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
ih : ∀ m < 0, F m = 0
⊢ Tendsto (fun x => ↑0 ^ ↑x * LSeries F ↑x) atTop (nhds (F 0))
Tactic:
refine Tendsto.congr' (H' 0).symm ?_
State after:
case neg.refine_1.ind.zero
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
ih : ∀ m < 0, F m = 0
⊢ Tendsto (fun x => 0) atTop (nhds (F 0))

State before:
case neg.refine_1.ind.zero
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
ih : ∀ m < 0, F m = 0
⊢ Tendsto (fun x => 0) atTop (nhds (F 0))
Tactic:
simp only [zero_eq, hF₀, tendsto_const_nhds_iff]
State after:
no goals

State before:
case neg.refine_1.ind.succ
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 + 1, F m = 0
⊢ Tendsto (fun x => ↑(n + 1) ^ ↑x * LSeries F ↑x) atTop (nhds (F (n + 1)))
Tactic:
simp only [succ_eq_add_one, cast_add, cast_one]
State after:
case neg.refine_1.ind.succ
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 + 1, F m = 0
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries F ↑x) atTop (nhds (F (n + 1)))

State before:
case neg.refine_1.ind.succ
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 + 1, F m = 0
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries F ↑x) atTop (nhds (F (n + 1)))
Tactic:
exact LSeries.tendsto_pow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <| Ne.lt_top ha
State after:
no goals

State before:
case neg.refine_2
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∀ (n : ℕ), n ≠ 0 → f n = 0
x : ℝ
⊢ (fun x => LSeries f ↑x) x = 0 x
Tactic:
simp only [LSeries_congr x fun {n} ↦ H n, show (fun _ : ℕ ↦ (0 : ℂ)) = 0 from rfl,
  LSeries_zero, Pi.zero_apply]
State after:
no goals