awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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
inl : Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds 0)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k / ((↑k : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑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]

Premises used: Real.inv_rpow, Complex.ofReal_cpow, div_eq_mul_inv, inv_div, Complex.ofReal_inv
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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
enter : 0
| Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds 0)

Tactic:
enter [3, 1]
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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
rw : f k * 0
| 0

Tactic:
rw [← mul_zero (f k)]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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
enter : f k * 0
| Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds 0)

Tactic:
enter [3, 1]; rw [← mul_zero (f k)]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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
inl : Tendsto (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds (f k * 0))
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ f k * (↑((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑k : ℝ)) ^ x) : ℂ)) atTop (nhds 0)

Tactic:
conv => enter [3, 1]; rw [← mul_zero (f k)]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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 (f k * 0))

Tactic:
(tendsto_rpow_atTop_of_base_lt_one _ (neg_one_lt_zero.trans_le H₀') H₂).ofReal.const_mul _

Premises used: tendsto_rpow_atTop_of_base_lt_one, Filter.Tendsto.const_mul, Filter.Tendsto.ofReal, LT.lt.trans_le, neg_one_lt_zero
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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 (f k * 0))

Tactic:
exact
        (tendsto_rpow_atTop_of_base_lt_one _ (neg_one_lt_zero.trans_le H₀') H₂).ofReal.const_mul _

Premises used: tendsto_rpow_atTop_of_base_lt_one, Filter.Tendsto.const_mul, Filter.Tendsto.ofReal, LT.lt.trans_le, neg_one_lt_zero
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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 : k ≤ n + 1
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ F x k) atTop (nhds 0)

Tactic:
simp [hF₀ _ H]
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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)

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]
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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)
rw : Tendsto (β := ℂ) (fun (x : ℝ) ↦ ∑' (m : ℕ), F x m) atTop (nhds (∑' (x : ℕ), 0))
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ ∑' (m : ℕ), F x m) atTop (nhds 0)

Tactic:
rw [show (0 : ℂ) = tsum (fun _ : ℕ ↦ 0) from tsum_zero.symm]

Premises used: tsum_zero, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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))

Tactic:
tendsto_tsum_of_dominated_convergence hys.norm hc <| eventually_iff.mpr ?_

Premises used: Iff.mpr, Filter.eventually_iff, tendsto_tsum_of_dominated_convergence, Summable.norm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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)
refine : Membership.mem (γ := Filter ℝ) atTop {x : ℝ | ∀ (k : ℕ), ‖F x k‖ ≤ ‖F y k‖}
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ ∑' (m : ℕ), F x m) atTop (nhds (∑' (x : ℕ), 0))

Tactic:
refine tendsto_tsum_of_dominated_convergence hys.norm hc <| eventually_iff.mpr ?_

Premises used: Iff.mpr, Filter.eventually_iff, tendsto_tsum_of_dominated_convergence, Summable.norm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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)
h₁ : ∀ (y' : ℝ) (hy' : y ≤ y') (k : ℕ), ‖F y' k‖ ≤ ‖F y k‖
⊢ Membership.mem (γ := Filter ℝ) atTop {x : ℝ | ∀ (k : ℕ), ‖F x k‖ ≤ ‖F y k‖}

Tactic:
filter_upwards [mem_atTop y] with y' hy' k

Premises used: Filter.mem_atTop
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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‖
h₂ : ∀ (H : k ≤ n + 1), ‖F y' k‖ ≤ ‖F y k‖
⊢ ‖F y' k‖ ≤ ‖F y k‖

Tactic:
rcases lt_or_ge (n + 1) k with H | H

Premises used: HAdd.hAdd, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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
h₁ :
  ‖f k‖ / ((↑k : ℝ) / ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖) ^ y' ≤ ‖f k‖ / ((↑k : ℝ) / ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖) ^ y
⊢ ‖F y' k‖ ≤ ‖F y k‖

Tactic:
simp only [Set.mem_setOf_eq, H, Set.indicator_of_mem, norm_div, norm_cpow_real,
      Complex.norm_natCast, F]

Premises used: Complex.norm_natCast, Complex.norm_cpow_real, Set.mem_setOf_eq, Set.indicator_of_mem, norm_div
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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
h₁ : ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y' ≤ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y
⊢ ‖f k‖ / ((↑k : ℝ) / ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖) ^ y' ≤ ‖f k‖ / ((↑k : ℝ) / ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖) ^ y

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, Complex.norm_natCast]

Premises used: Complex.norm_natCast, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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
⊢ LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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
⊢ 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
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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‖
h₂ : 0 < HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y
h₃ : 1 ≤ HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ)
⊢ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y' ≤ ‖f k‖ / HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(n + 1) : ℝ) ^ y

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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 : k ≤ n + 1
⊢ ‖F y' k‖ ≤ ‖F y k‖

Tactic:
simp [hF₀ _ H]
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
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 : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
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