awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < (↑y : EReal)
hyt : (↑y : EReal) < ⊤
F : (x : ℝ) → (x : ℕ) → ℂ :=
  fun (x : ℝ) ↦
    Set.indicator {m : ℕ | n + 1 < m} fun (m : ℕ) ↦ f m / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
hF₀ : ∀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1), F x m = 0
hF : ∀ (x : ℝ) {m : ℕ} (hm : m ≠ n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
hs :
  ∀ {x : ℝ} (hx : x ≥ y), Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
key : ∀ x ≥ y, HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
⊢ ‖F y' k‖ ≤ ‖F y k‖
have h₁ : ∀ (H : n + 1 < k), ‖F y' k‖ ≤ ‖F y k‖
Tactic: rcases lt_or_ge (n + 1) k with H | H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < (↑y : EReal)
hyt : (↑y : EReal) < ⊤
F : (x : ℝ) → (x : ℕ) → ℂ :=
  fun (x : ℝ) ↦
    Set.indicator {m : ℕ | n + 1 < m} fun (m : ℕ) ↦ f m / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
hF₀ : ∀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1), F x m = 0
hF : ∀ (x : ℝ) {m : ℕ} (hm : m ≠ n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
hs :
  ∀ {x : ℝ} (hx : x ≥ y), Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
key : ∀ x ≥ y, HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
h₁ : ∀ (H : n + 1 < k), ‖F y' k‖ ≤ ‖F y k‖
⊢ ‖F y' k‖ ≤ ‖F y k‖
have h₂ : ∀ (H : k ≤ n + 1), ‖F y' k‖ ≤ ‖F y k‖
Tactic: rcases lt_or_ge (n + 1) k with H | H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < (↑y : EReal)
hyt : (↑y : EReal) < ⊤
F : (x : ℝ) → (x : ℕ) → ℂ :=
  fun (x : ℝ) ↦
    Set.indicator {m : ℕ | n + 1 < m} fun (m : ℕ) ↦ f m / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
hF₀ : ∀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1), F x m = 0
hF : ∀ (x : ℝ) {m : ℕ} (hm : m ≠ n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
hs :
  ∀ {x : ℝ} (hx : x ≥ y), Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
key : ∀ x ≥ y, HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : n + 1 < k
⊢ ‖F y' k‖ ≤ ‖F y k‖
have h₁ : ‖f k‖ / ((↑k : ℝ) / ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖) ^ y' ≤ ‖f k‖ / ((↑k : ℝ) / ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖) ^ y
Tactic: simp only [Set.mem_setOf_eq, H, Set.indicator_of_mem, norm_div, norm_cpow_real,
      Complex.norm_natCast, F]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < (↑y : EReal)
hyt : (↑y : EReal) < ⊤
F : (x : ℝ) → (x : ℕ) → ℂ :=
  fun (x : ℝ) ↦
    Set.indicator {m : ℕ | n + 1 < m} fun (m : ℕ) ↦ f m / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
hF₀ : ∀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1), F x m = 0
hF : ∀ (x : ℝ) {m : ℕ} (hm : m ≠ n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
hs :
  ∀ {x : ℝ} (hx : x ≥ y), Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
key : ∀ x ≥ y, HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : n + 1 < k
⊢ ‖f k‖ / ((↑k : ℝ) / ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖) ^ y' ≤ ‖f k‖ / ((↑k : ℝ) / ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖) ^ y
have h₁ : ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y' ≤ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, Complex.norm_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < (↑y : EReal)
hyt : (↑y : EReal) < ⊤
F : (x : ℝ) → (x : ℕ) → ℂ :=
  fun (x : ℝ) ↦
    Set.indicator {m : ℕ | n + 1 < m} fun (m : ℕ) ↦ f m / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
hF₀ : ∀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1), F x m = 0
hF : ∀ (x : ℝ) {m : ℕ} (hm : m ≠ n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
hs :
  ∀ {x : ℝ} (hx : x ≥ y), Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
key : ∀ x ≥ y, HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : n + 1 < k
⊢ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y' ≤ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y
have hkn : 1 ≤ HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ)
Tactic: have hkn : 1 ≤ (k / (n + 1 :) : ℝ) :=
      (one_le_div (by positivity)).mpr <| mod_cast Nat.le_of_succ_le H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < (↑y : EReal)
hyt : (↑y : EReal) < ⊤
F : (x : ℝ) → (x : ℕ) → ℂ :=
  fun (x : ℝ) ↦
    Set.indicator {m : ℕ | n + 1 < m} fun (m : ℕ) ↦ f m / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
hF₀ : ∀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1), F x m = 0
hF : ∀ (x : ℝ) {m : ℕ} (hm : m ≠ n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
hs :
  ∀ {x : ℝ} (hx : x ≥ y), Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
key : ∀ x ≥ y, HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : n + 1 < k
hkn : 1 ≤ HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ)
⊢ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y' ≤ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y
have h₁ : 0 ≤ ‖f k‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < (↑y : EReal)
hyt : (↑y : EReal) < ⊤
F : (x : ℝ) → (x : ℕ) → ℂ :=
  fun (x : ℝ) ↦
    Set.indicator {m : ℕ | n + 1 < m} fun (m : ℕ) ↦ f m / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
hF₀ : ∀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1), F x m = 0
hF : ∀ (x : ℝ) {m : ℕ} (hm : m ≠ n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
hs :
  ∀ {x : ℝ} (hx : x ≥ y), Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
key : ∀ x ≥ y, HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : n + 1 < k
hkn : 1 ≤ HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ)
h₁ : 0 ≤ ‖f k‖
⊢ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y' ≤ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y
have h₂ : 0 < HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
Goal:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
⊢ Tendsto (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) atTop (nhds (f 1))
have hF₀ : F 0 = 0
Tactic: have hF₀ : F 0 = 0 := rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
Goal:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : (n : ℕ) → ℂ := fun (n : ℕ) ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
⊢ Tendsto (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) atTop (nhds (f 1))
have hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
Tactic: have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) atTop (nhds (f 1))
have ha' : abscissaOfAbsConv F < ⊤
Tactic: have ha' : abscissaOfAbsConv F < ⊤ := (abscissaOfAbsConv_congr hF).symm ▸ ha
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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 : ℝ) ↦ LSeries f (↑x : ℂ)) atTop (nhds (f 1))
have simp_rw : Tendsto (fun (x : ℝ) ↦ LSeries F (↑x : ℂ)) atTop (nhds (f 1))
Tactic: simp_rw [← LSeries_congr hF]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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 : ℝ) ↦ LSeries F (↑x : ℂ)) atTop (nhds (f 1))
have h : Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ LSeries F (↑x : ℂ)) fun (x : ℝ) ↦
  HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 ^ (↑x : ℂ) * LSeries F (↑x : ℂ)
Tactic: convert! LSeries.tendsto_cpow_mul_atTop (n := 0) (fun _ hm ↦ Nat.le_zero.mp hm ▸ hF₀) ha' using 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0
have h₁ : ∀ (s : ℂ), LSeries f s = 0 s
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔
    (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤
have pos : ∀ (h : abscissaOfAbsConv f = ⊤),
  EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔
    (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤
Tactic: by_cases h : abscissaOfAbsConv f = ⊤
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
pos :
  ∀ (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 = ⊤
have neg : ∀ (h : ¬abscissaOfAbsConv f = ⊤),
  EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔
    (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤
Tactic: by_cases h : abscissaOfAbsConv f = ⊤
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔
    (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤
have neg : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔ ∀ (n : ℕ), ¬n = 0 → f n = 0
Tactic: simp only [ne_eq, h, or_false]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) 0 ↔ ∀ (n : ℕ), ¬n = 0 → f n = 0
have neg : ∀ (H : 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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
neg : ∀ (H : 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
have neg₁ : ∀ (H : ∀ (n : ℕ), ¬n = 0 → f n = 0) (x : ℝ), Eq (α := ℂ) ((fun (x : ℝ) ↦ LSeries f (↑x : ℂ)) x) (0 x)
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ Eventually.of_forall fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
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
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0
have hF₀ : F 0 = 0
Tactic: have hF₀ : F 0 = 0 := rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
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 : ℕ), ¬n = 0 → f n = 0
have hF : ∀ {n : ℕ} (hn : n ≠ 0), F n = f n
Tactic: have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0
have neg : ∀ (n : ℕ), F n = 0
Tactic: suffices ∀ n, F n = 0 from fun n hn ↦ (hF hn).symm.trans (this n)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
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
⊢ ∀ (n : ℕ), F n = 0
have ha : ¬abscissaOfAbsConv F = ⊤
Tactic: have ha : ¬ abscissaOfAbsConv F = ⊤ := abscissaOfAbsConv_congr hF ▸ h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
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 = ⊤
⊢ ∀ (n : ℕ), F n = 0
have h' : ∀ (x : ℝ), LSeries F (↑x : ℂ) = LSeries f (↑x : ℂ)
Tactic: have h' (x : ℝ) : LSeries F x = LSeries f x := LSeries_congr hF x
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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
have simp : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries f (↑x : ℂ)) fun (x : ℝ) ↦ 0
Tactic: simp only [h']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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
have 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
Tactic: rw [eventuallyEq_iff_exists_mem] at H ⊢
Cleared hypotheses: H, F, hF₀, hF, ha, h', n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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 : ℕ
⊢ ∃ (s : Set ℝ),
    Membership.mem (γ := Filter ℝ) atTop s ∧
      Set.EqOn (β := ℂ) (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries f (↑x : ℂ)) (fun (x : ℝ) ↦ 0) s
have 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
Tactic: obtain ⟨s, hs⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
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 : ℕ), F n = 0
have H' : ∀ (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]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
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))
⊢ F n = 0
have this₁ : Tendsto (fun (x : ℝ) ↦ 0) atTop (nhds (F n))
Tactic: replace this := this.congr' <| H' n
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
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))
⊢ F n = 0
have this₁ : 0 = F n
Tactic: simp only [tendsto_const_nhds_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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
⊢ F n = 0
have neg : Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F n))
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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F n))
have neg : ∀ (ih : ∀ m < 0, F m = 0),
  Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑0 : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F 0))
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
Cleared hypotheses: n, ih
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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))
⊢ Tendsto (fun (x : ℝ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ) * LSeries F (↑x : ℂ)) atTop (nhds (F n))
have 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)))
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
Cleared hypotheses: n, ih
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
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 : ℕ
⊢ F n = 0
have neg : ∀ (n : ℕ) (ih : ∀ m < n, F m = 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
have pos : ∀ (h : abscissaOfAbsConv f = ⊤), LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
Tactic: by_cases h : abscissaOfAbsConv f = ⊤