awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
e_a : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (-(↑x : ℂ))
e_a₁ :
  (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
    (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ ((↑(-1) : ℂ) * (↑x : ℂ))
e_a₂ :
  (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
    (↑(HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ (-1)) : ℂ) ^ (↑x : ℂ)
⊢ (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
have e_a₃ : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹⁻¹ : ℂ) ^ (↑x : ℂ)
Tactic: rw [← cpow_neg, show (-x : ℂ) = (-1 : ℝ) * x by simp, cpow_mul_ofReal_nonneg Hn,
    Real.rpow_neg_one, inv_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
e_a : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (-(↑x : ℂ))
e_a₁ :
  (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
    (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ ((↑(-1) : ℂ) * (↑x : ℂ))
e_a₂ :
  (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
    (↑(HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ (-1)) : ℂ) ^ (↑x : ℂ)
e_a₃ : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹⁻¹ : ℂ) ^ (↑x : ℂ)
⊢ (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
have e_a₄ : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ)
Tactic: rw [← cpow_neg, show (-x : ℂ) = (-1 : ℝ) * x by simp, cpow_mul_ofReal_nonneg Hn,
    Real.rpow_neg_one, inv_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
have obtain : ∀ (y : EReal) (hay : abscissaOfAbsConv f < y) (hyt : y < ⊤),
  Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
Tactic: obtain ⟨y, hay, hyt⟩ := exists_between ha
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : EReal
hay : abscissaOfAbsConv f < y
hyt : y < ⊤
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
have lift : ∀ (y : ℝ) (hay : abscissaOfAbsConv f < (↑y : EReal)) (hyt : (↑y : EReal) < ⊤),
  Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
Tactic: lift y to ℝ using ⟨hyt.ne, ((OrderBot.bot_le _).trans_lt hay).ne'⟩
Cleared hypotheses: y, hay, hyt
-- 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 : ℂ)
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
have hF₀ : ∀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1), F x m = 0
Tactic: have hF₀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1) : F x m = 0 := by simp [F, not_lt_of_ge hm]
-- 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
x : ℝ
m : ℕ
hm : m ≠ n + 1
⊢ F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
have inl : ∀ (H : m < n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
Tactic: rcases lt_trichotomy m (n + 1) with H | rfl | 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
x : ℝ
m : ℕ
hm : m ≠ n + 1
inl : ∀ (H : m < n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
⊢ F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
have inr : ∀ (hm : n + 1 ≠ n + 1), F x (n + 1) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) (n + 1)
Tactic: rcases lt_trichotomy m (n + 1) with H | rfl | H
Cleared hypotheses: m, hm
-- 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
x : ℝ
m : ℕ
hm : m ≠ n + 1
inl : ∀ (H : m < n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
inr : ∀ (hm : n + 1 ≠ n + 1), F x (n + 1) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) (n + 1)
⊢ F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
have inr₁ : ∀ (H : n + 1 < m), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
Tactic: rcases lt_trichotomy m (n + 1) with H | rfl | 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
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
have hF : ∀ (x : ℝ) {m : ℕ} (hm : m ≠ n + 1), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
Tactic: have hF (x : ℝ) {m : ℕ} (hm : m ≠ n + 1) : F x m = ((n + 1) ^ (x : ℂ)) * term f x m := by
    rcases lt_trichotomy m (n + 1) with H | rfl | H
    · simp [Nat.not_lt_of_gt H, term, h m <| Nat.lt_succ_iff.mp H, F]
    · exact (hm rfl).elim
    · simp [H, term, (n.zero_lt_succ.trans H).ne', F, cpow_mul_div_cpow_eq_div_div_cpow]
-- 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
x : ℝ
hx : x ≥ y
⊢ Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
have refine : abscissaOfAbsConv f < (↑(↑x : ℂ).re : EReal)
Tactic: refine (summable_mul_left_iff <| natCast_add_one_cpow_ne_zero n _).mpr <|
       LSeriesSummable_of_abscissaOfAbsConv_lt_re ?_
-- 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
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
have hs : ∀ {x : ℝ} (hx : x ≥ y), Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
Tactic: have hs {x : ℝ} (hx : x ≥ y) : Summable fun m ↦ (n + 1) ^ (x : ℂ) * term f x m := by
    refine (summable_mul_left_iff <| natCast_add_one_cpow_ne_zero n _).mpr <|
       LSeriesSummable_of_abscissaOfAbsConv_lt_re ?_
    simpa only [ofReal_re] using hay.trans_le <| EReal.coe_le_coe_iff.mpr hx
-- 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
x : ℝ
hx : x ≥ y
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = f (n + 1) + ∑' (m : ℕ), F x m
have rw : (f (n + 1) + ∑' (n_1 : ℕ), if n_1 = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) n_1) =
  f (n + 1) + ∑' (m : ℕ), F x m
Tactic: rw [LSeries, ← tsum_mul_left, (hs hx).tsum_eq_add_tsum_ite (n + 1), pow_mul_term_eq f x n]
-- 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
x : ℝ
hx : x ≥ y
⊢ (f (n + 1) +
      ∑' (n_1 : ℕ), if n_1 = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) n_1) =
    f (n + 1) + ∑' (m : ℕ), F x m
have e_a : Eq (α := ℕ → ℂ)
  (fun (n_1 : ℕ) ↦ if n_1 = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) n_1)
  fun (m : ℕ) ↦ F x m
Tactic: congr
-- 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
x : ℝ
hx : x ≥ y
⊢ Eq (α := ℕ → ℂ)
    (fun (n_1 : ℕ) ↦ if n_1 = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) n_1)
    fun (m : ℕ) ↦ F x m
have e_a : ∀ (m : ℕ), (if m = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m) = F x m
Tactic: ext1 m
-- 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
x : ℝ
hx : x ≥ y
m : ℕ
⊢ (if m = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m) = F x m
have e_a : (if n + 1 = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) (n + 1)) = F x (n + 1)
Tactic: rcases eq_or_ne m (n + 1) with rfl | hm
Cleared hypotheses: m
-- 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
x : ℝ
hx : x ≥ y
m : ℕ
e_a : (if n + 1 = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) (n + 1)) = F x (n + 1)
⊢ (if m = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m) = F x m
have e_a₁ : ∀ (hm : m ≠ n + 1), (if m = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m) = F x m
Tactic: rcases eq_or_ne m (n + 1) with rfl | hm
-- 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
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
have key : ∀ x ≥ y, HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = f (n + 1) + ∑' (m : ℕ), F x m
Tactic: have key : ∀ x ≥ y, (n + 1) ^ (x : ℂ) * LSeries f x = f (n + 1) + ∑' m : ℕ, F x m := by
    intro x hx
    rw [LSeries, ← tsum_mul_left, (hs hx).tsum_eq_add_tsum_ite (n + 1), pow_mul_term_eq f x n]
    congr
    ext1 m
    rcases eq_or_ne m (n + 1) with rfl | hm
    · simp [hF₀ x le_rfl]
    · simp [hm, hF]
-- 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
| Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
have enter : f (n + 1)
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
| f (n + 1)
have rw : f (n + 1) + 0
Tactic: rw [← add_zero (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
| Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
have enter : f (n + 1) + 0
Tactic: enter [3, 1]; rw [← add_zero (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
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))
have conv : Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1) + 0))
Tactic: conv => enter [3, 1]; rw [← add_zero (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
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1) + 0))
have refine : Tendsto (β := ℂ) (fun (x : ℝ) ↦ ∑' (m : ℕ), F x m) atTop (nhds 0)
Tactic: refine Tendsto.congr'
    (eventuallyEq_of_mem (s := {x | y ≤ x}) (mem_atTop y) key).symm <| tendsto_const_nhds.add ?_
-- 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
⊢ Summable (F y)
have refine : ∀ (m : ℕ),
  Set.indicator {m : ℕ | n + 1 < m} (fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑y : ℂ) * term f (↑y : ℂ) m) m =
    F y m
Tactic: refine ((hs le_rfl).indicator {m | n + 1 < m}).congr fun m ↦ ?_
-- 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
m : ℕ
⊢ Set.indicator {m : ℕ | n + 1 < m} (fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑y : ℂ) * term f (↑y : ℂ) m) m =
    F y m
have pos : ∀ (hm : n + 1 < m),
  Set.indicator {m : ℕ | n + 1 < m} (fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑y : ℂ) * term f (↑y : ℂ) m) m =
    F y m
Tactic: by_cases! hm : n + 1 < m
-- 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
m : ℕ
pos :
  ∀ (hm : n + 1 < m),
    Set.indicator {m : ℕ | n + 1 < m} (fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑y : ℂ) * term f (↑y : ℂ) m) m =
      F y m
⊢ Set.indicator {m : ℕ | n + 1 < m} (fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑y : ℂ) * term f (↑y : ℂ) m) m =
    F y m
have neg : ∀ (hm : m ≤ n + 1),
  Set.indicator {m : ℕ | n + 1 < m} (fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑y : ℂ) * term f (↑y : ℂ) m) m =
    F y m
Tactic: by_cases! hm : n + 1 < m
-- 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
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ ∑' (m : ℕ), F x m) atTop (nhds 0)
have hys : Summable (F y)
Tactic: have hys : Summable (F y) := by
    refine ((hs le_rfl).indicator {m | n + 1 < m}).congr fun m ↦ ?_
    by_cases! hm : n + 1 < m
    · simp [hF, hm, hm.ne']
    · simp [hm, hF₀ _ hm]