awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
⊢ abscissaOfAbsConv F < ⊤

Tactic:
have ha' : abscissaOfAbsConv F < ⊤ := (abscissaOfAbsConv_congr hF).symm ▸ ha
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha' : abscissaOfAbsConv F < ⊤
simp_rw : Tendsto (fun (x : ℝ) ↦ LSeries F (↑x : ℂ)) atTop (nhds (f 1))
⊢ Tendsto (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) atTop (nhds (f 1))

Tactic:
simp_rw [← LSeries_congr hF]

Premises used: LSeries_congr
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 ^ (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop
    (nhds (F (HAdd.hAdd (α := ℕ) 0 1)))

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

Premises used: LSeries.tendsto_cpow_mul_atTop
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha' : abscissaOfAbsConv F < ⊤
h :
  Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
    HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 ^ (↑x : ℂ) * LSeries F (↑x : ℂ)
⊢ 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

Premises used: LSeries.tendsto_cpow_mul_atTop
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
    HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 ^ (↑x : ℂ) * LSeries F (↑x : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
h₁ : ∀ (s : ℂ), LSeries f s = 0 s
⊢ LSeries f = 0

Tactic:
ext1 s
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s

Tactic:
LSeries.eq_zero_of_not_LSeriesSummable f s <| mt LSeriesSummable.abscissaOfAbsConv_le <|
    h ▸ fun H ↦ (H.trans_lt <| EReal.coe_lt_top _).false

Premises used: LSeriesSummable.abscissaOfAbsConv_le, mt, Eq.rec, Complex.re, LT.lt.false, Eq.symm, LSeries.eq_zero_of_not_LSeriesSummable, LE.le.trans_lt, EReal.coe_lt_top
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s

Tactic:
exact LSeries.eq_zero_of_not_LSeriesSummable f s <| mt LSeriesSummable.abscissaOfAbsConv_le <|
    h ▸ fun H ↦ (H.trans_lt <| EReal.coe_lt_top _).false

Premises used: LSeriesSummable.abscissaOfAbsConv_le, mt, LSeries.eq_zero_of_not_LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
pos :
  ∀ (h : abscissaOfAbsConv f = ⊤),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔
      (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤
neg :
  ∀ (h : ¬abscissaOfAbsConv f = ⊤),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔
      (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔
    (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤

Tactic:
by_cases h : abscissaOfAbsConv f = ⊤

Premises used: LSeries.abscissaOfAbsConv
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ ∀ (x : ℝ), Eq (α := ℂ) ((fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) x) (0 x)

Tactic:
simp [LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h]

Premises used: LSeries_eq_zero_of_abscissaOfAbsConv_eq_top
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔
    (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤

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

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
neg : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔ ∀ (n : ℕ), ¬n = 0 → f n = 0
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔
    (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤

Tactic:
simp only [ne_eq, h, or_false]

Premises used: ne_eq, or_false
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔ ∀ (n : ℕ), ¬n = 0 → f n = 0

Tactic:
⟨fun H ↦ ?_, fun H ↦ Eventually.of_forall fun x ↦ ?_⟩

Premises used: Filter.Eventually.of_forall, Iff.intro
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
neg : ∀ (H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0) (n : ℕ), ¬n = 0 → f n = 0
neg₁ : ∀ (H : ∀ (n : ℕ), ¬n = 0 → f n = 0) (x : ℝ), Eq (α := ℂ) ((fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) x) (0 x)
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔ ∀ (n : ℕ), ¬n = 0 → f n = 0

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ Eventually.of_forall fun x ↦ ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
⊢ F 0 = 0

Tactic:
have hF₀ : F 0 = 0 := rfl
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
⊢ ∀ {n : ℕ} (hn : n ≠ 0), F n = f n

Tactic:
have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
neg : ∀ (n : ℕ), F n = 0
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

Tactic:
suffices ∀ n, F n = 0 from fun n hn ↦ (hF hn).symm.trans (this n)
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
⊢ ¬abscissaOfAbsConv F = ⊤

Tactic:
have ha : ¬ abscissaOfAbsConv F = ⊤ := abscissaOfAbsConv_congr hF ▸ h
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
⊢ ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)

Tactic:
have h' (x : ℝ) : LSeries F x = LSeries f x := LSeries_congr hF x
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
n : ℕ
simp :
  EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ 0
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦ 0

Tactic:
simp only [h']
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
n : ℕ
rw :
  ∀
    (H :
      ∃ (s : Set ℝ), Membership.mem (γ := Filter ℝ) atTop s ∧ Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 s),
    let F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n;
    ∀ (hF₀ : F 0 = 0) (hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n) (ha : ¬abscissaOfAbsConv F = ⊤)
      (h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)) (n : ℕ),
      ∃ (s : Set ℝ),
        Membership.mem (γ := Filter ℝ) atTop s ∧
          Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries f (↑x : ℂ)) (fun (x : ℝ) ↦ 0)
            s
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ 0

Tactic:
rw [eventuallyEq_iff_exists_mem] at H ⊢

Premises used: Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∃ (s : Set ℝ), Membership.mem (γ := Filter ℝ) atTop s ∧ Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 s
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
n : ℕ
obtain :
  ∀ (s : Set ℝ)
    (hs : Membership.mem (γ := Filter ℝ) atTop s ∧ Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 s),
    ∃ (s : Set ℝ),
      Membership.mem (γ := Filter ℝ) atTop s ∧
        Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries f (↑x : ℂ)) (fun (x : ℝ) ↦ 0) s
⊢ ∃ (s : Set ℝ),
    Membership.mem (γ := Filter ℝ) atTop s ∧
      Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries f (↑x : ℂ)) (fun (x : ℝ) ↦ 0) s

Tactic:
obtain ⟨s, hs⟩ := H
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
n : ℕ
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) atTop s ∧ Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 s
x : ℝ
hx : x ∈ s
⊢ Eq (α := ℂ) ((fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries f (↑x : ℂ)) x) ((fun (x : ℝ) ↦ (0 : ℂ)) x)

Tactic:
simp [hs.2 hx]

Premises used: And.right
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
n : ℕ
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) atTop s ∧ Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 s
⊢ ∃ (s : Set ℝ),
    Membership.mem (γ := Filter ℝ) atTop s ∧
      Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries f (↑x : ℂ)) (fun (x : ℝ) ↦ 0) s

Tactic:
exact ⟨s, hs.1, fun x hx ↦ by simp [hs.2 hx]⟩
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
⊢ ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      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]⟩
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
n : ℕ
ih : ∀ m < n, F m = 0
this : Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F n))
⊢ Tendsto (fun (x : ℝ) ↦ 0) atTop (nhds (F n))

Tactic:
replace this := this.congr' <| H' n
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
n : ℕ
ih : ∀ m < n, F m = 0
this : Tendsto (fun (x : ℝ) ↦ 0) atTop (nhds (F n))
⊢ 0 = F n

Tactic:
simp only [tendsto_const_nhds_iff] at this

Premises used: tendsto_const_nhds_iff
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
n : ℕ
ih : ∀ m < n, F m = 0
this : 0 = F n
⊢ F n = 0

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
n : ℕ
ih : ∀ m < n, F m = 0
this : 0 = F n
⊢ F n = 0

Tactic:
exact this.symm

Premises used: Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
n : ℕ
ih : ∀ m < n, F m = 0
neg : Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F n))
⊢ 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
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
ih : ∀ m < 0, F m = 0
⊢ Tendsto (fun (x : ℝ) ↦ 0) atTop (nhds (F 0))

Tactic:
simp [hF₀]
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
ih : ∀ m < 0, F m = 0
⊢ Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑0 : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F 0))

Tactic:
exact Tendsto.congr' (H' 0).symm <| by simp [hF₀]

Premises used: Filter.Tendsto.congr', OfNat.ofNat, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
n : ℕ
ih : ∀ m < n + 1, F m = 0
⊢ Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑(n + 1) : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F (n + 1)))

Tactic:
simpa using LSeries.tendsto_cpow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <|
            Ne.lt_top ha

Premises used: Nat.lt_succ_of_le, Ne.lt_top, LSeries.tendsto_cpow_mul_atTop
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
n : ℕ
ih : ∀ m < n, F m = 0
neg :
  ∀ (ih : ∀ m < 0, F m = 0),
    Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑0 : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F 0))
neg₁ :
  ∀ (n : ℕ) (ih : ∀ m < n + 1, F m = 0),
    Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑(n + 1) : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F (n + 1)))
⊢ Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F n))

Tactic:
cases n with
      | zero => exact Tendsto.congr' (H' 0).symm <| by simp [hF₀]
      | succ n =>
          simpa using LSeries.tendsto_cpow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <|
            Ne.lt_top ha

Premises used: Ne.lt_top, Nat.zero, Filter.Tendsto.congr', OfNat.ofNat, Nat.succ, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
H' :
  ∀ (n : ℕ),
    EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
      0
n : ℕ
neg : ∀ (n : ℕ) (ih : ∀ m < n, F m = 0), F n = 0
⊢ F n = 0

Tactic:
induction n using Nat.strongRecOn with | ind n ih =>
      -- it suffices to show that `n ^ x * LSeries F x` tends to `F n` as `x` tends to `∞`
      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
      cases n with
      | zero => exact Tendsto.congr' (H' 0).symm <| by simp [hF₀]
      | succ n =>
          simpa using LSeries.tendsto_cpow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <|
            Ne.lt_top ha

Premises used: Ne.lt_top, Nat.zero, Filter.Tendsto.congr', OfNat.ofNat, Nat.succ, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∀ (n : ℕ), ¬n = 0 → f n = 0
x : ℝ
⊢ Eq (α := ℂ) ((fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) x) (0 x)

Tactic:
simp [LSeries_congr (fun {n} ↦ H n) x, show (fun _ : ℕ ↦ (0 : ℂ)) = 0 from rfl]

Premises used: LSeries_congr, Complex.ofReal, rfl
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
pos : ∀ (h : abscissaOfAbsConv f = ⊤), LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
neg : ∀ (h : ¬abscissaOfAbsConv f = ⊤), LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤

Tactic:
by_cases h : abscissaOfAbsConv f = ⊤

Premises used: LSeries.abscissaOfAbsConv
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤

Tactic:
simpa [h] using LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h

Premises used: LSeries_eq_zero_of_abscissaOfAbsConv_eq_top
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
neg : LSeries f = 0 ↔ f = 0
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤

Tactic:
simp only [h, or_false]

Premises used: or_false
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0

Tactic:
⟨fun H ↦ ?_, fun H ↦ H ▸ LSeries_zero⟩

Premises used: Eq.rec, Iff.intro, LSeries_zero, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
neg : ∀ (H : LSeries f = 0), f = 0
⊢ LSeries f = 0 ↔ f = 0

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H ▸ LSeries_zero⟩
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ ∀ (n : ℕ), n ≠ 0 → f n = 0

Tactic:
(LSeries_eventually_eq_zero_iff'.mp ?_).resolve_right h

Premises used: LSeries_eventually_eq_zero_iff', Iff.mp, Or.resolve_right
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
a : f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0
neg : Filter.EventuallyEq (β := ℂ) Filter.atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0
⊢ f = 0

Tactic:
convert! (LSeries_eventually_eq_zero_iff'.mp ?_).resolve_right h

Premises used: LSeries_eventually_eq_zero_iff', Iff.mp, Or.resolve_right
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : f = 0
x : ℕ
h_1 : x ≠ 0
rw : Eq (α := ℂ) (0 x) 0
rw₁ rw₂ : Eq (α := ℂ) 0 0
⊢ f x = 0

Tactic:
rw [H', Pi.zero_apply]

Premises used: Pi.zero_apply
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
a : ∀ (H' : ∀ (n : ℕ), n ≠ 0 → f n = 0), f = 0
⊢ f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0

Tactic:
refine ⟨fun H' _ _ ↦ by rw [H', Pi.zero_apply], fun H' ↦ ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
a : f 0 = 0 0
a₁ : ∀ (m : ℕ), f (m + 1) = 0 (m + 1)
⊢ f = 0

Tactic:
ext (- | m)
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0

Tactic:
simp [hf]
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
m : ℕ
⊢ f (m + 1) = 0 (m + 1)

Tactic:
simp [H']