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)
k : ℕ
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
have inl : ∀ (H : n + 1 < k), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
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)
k : ℕ
inl : ∀ (H : n + 1 < k), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
have inr : ∀ (H : k ≤ n + 1), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
Tactic: rcases lt_or_ge (n + 1) k with H | H
-- 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)
k : ℕ
H : n + 1 < k
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
have H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: have H₀ : (0 : ℝ) ≤ k / (n + 1) := by positivity
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
have H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
Tactic: have H₀' : (0 : ℝ) ≤ (n + 1) / k := by positivity
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
⊢ (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
have push_cast : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
Tactic: push_cast
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
have H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
Tactic: have H₁ : (k / (n + 1) : ℂ) = (k / (n + 1) : ℝ) := by push_cast; rfl
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
have H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
Tactic: have H₂ : (n + 1) / k < (1 : ℝ) :=
        (div_lt_one <| mod_cast n.succ_pos.trans H).mpr <| mod_cast 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
have inl : Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k / ((↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)) atTop (nhds 0)
Tactic: simp only [Set.mem_setOf_eq, H, Set.indicator_of_mem, 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
| Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k / ((↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)) atTop (nhds 0)
have h₁ : ∀ (x : ℝ), f k / ((↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
Tactic: enter [1, x]
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
x : ℝ
| f k / ((↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
have h₁ : f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)
Tactic: rw [div_eq_mul_inv, H₁, ← ofReal_cpow H₀, ← ofReal_inv, ← Real.inv_rpow H₀, inv_div]
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
| Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k / ((↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)) atTop (nhds 0)
have h₁ : ∀ (x : ℝ), f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)
Tactic: enter [1, x]
        rw [div_eq_mul_inv, H₁, ← ofReal_cpow H₀, ← ofReal_inv, ← Real.inv_rpow H₀, inv_div]
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k / ((↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)) atTop (nhds 0)
have inl : Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds 0)
Tactic: conv =>
        enter [1, x]
        rw [div_eq_mul_inv, H₁, ← ofReal_cpow H₀, ← ofReal_inv, ← Real.inv_rpow H₀, inv_div]
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
| Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds 0)
have enter : 0
Tactic: enter [3, 1]
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
| 0
have rw : f k * 0
Tactic: rw [← mul_zero (f k)]
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
| Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds 0)
have enter : f k * 0
Tactic: enter [3, 1]; rw [← mul_zero (f k)]
-- 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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ (↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
H₀' : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)
H₁ : (↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑((↑k : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
H₂ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ) < 1
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds 0)
have inl : Tendsto (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds (f k * 0))
Tactic: conv => enter [3, 1]; rw [← mul_zero (f k)]
-- 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)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ ∑' (m : ℕ), F x m) atTop (nhds 0)
have hc : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)
Tactic: have hc (k : ℕ) : Tendsto (F · k) atTop (nhds 0) := by
    rcases lt_or_ge (n + 1) k with H | H
    · have H₀ : (0 : ℝ) ≤ k / (n + 1) := by positivity
      have H₀' : (0 : ℝ) ≤ (n + 1) / k := by positivity
      have H₁ : (k / (n + 1) : ℂ) = (k / (n + 1) : ℝ) := by push_cast; rfl
      have H₂ : (n + 1) / k < (1 : ℝ) :=
        (div_lt_one <| mod_cast n.succ_pos.trans H).mpr <| mod_cast H
      simp only [Set.mem_setOf_eq, H, Set.indicator_of_mem, F]
      conv =>
        enter [1, x]
        rw [div_eq_mul_inv, H₁, ← ofReal_cpow H₀, ← ofReal_inv, ← Real.inv_rpow H₀, inv_div]
      conv => enter [3, 1]; rw [← mul_zero (f k)]
      exact
        (tendsto_rpow_atTop_of_base_lt_one _ (neg_one_lt_zero.trans_le H₀') H₂).ofReal.const_mul _
    · simp [hF₀ _ 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)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ ∑' (m : ℕ), F x m) atTop (nhds 0)
have rw : Tendsto (β := ℂ) (fun (x : ℝ) ↦ ∑' (m : ℕ), F x m) atTop (nhds (∑' (x : ℕ), 0))
Tactic: rw [show (0 : ℂ) = tsum (fun _ : ℕ ↦ 0) from tsum_zero.symm]
-- 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)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ ∑' (m : ℕ), F x m) atTop (nhds (∑' (x : ℕ), 0))
have refine : Membership.mem (γ := Filter ℝ) atTop {x : ℝ | ∀ (k : ℕ), ‖F x k‖ ≤ ‖F y k‖}
Tactic: refine tendsto_tsum_of_dominated_convergence hys.norm hc <| eventually_iff.mpr ?_
-- 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)
⊢ Membership.mem (γ := Filter ℝ) atTop {x : ℝ | ∀ (k : ℕ), ‖F x k‖ ≤ ‖F y k‖}
have h₁ : ∀ (y' : ℝ) (hy' : y ≤ y') (k : ℕ), ‖F y' k‖ ≤ ‖F y k‖
Tactic: filter_upwards [mem_atTop y] with y' hy' k