awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
rw :
  z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) / HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ)) =
    z * (((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ))⁻¹
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * (z / HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ)) =
    z / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)

Tactic:
rw [← mul_div_assoc, mul_comm, div_eq_mul_inv z, mul_div_assoc]

Premises used: mul_div_assoc, div_eq_mul_inv, mul_comm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
e_a :
  HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) / HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ) =
    (((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ))⁻¹
⊢ z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) / HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ)) =
    z * (((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ))⁻¹

Tactic:
congr
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : n + 1 = n + 1
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : m = m
⊢ (↑m : ℂ) = (↑(↑m : ℝ) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
e_a :
  ((↑(↑m : ℝ) : ℂ) ^ (↑x : ℂ))⁻¹ * (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
    ((↑(↑m : ℝ) : ℂ) ^ (↑x : ℂ))⁻¹ * ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * (HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ))⁻¹ =
    (((↑m : ℂ) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹) ^ (↑x : ℂ))⁻¹

Tactic:
rw [show (n + 1 : ℂ)⁻¹ = (n + 1 : ℝ)⁻¹ by simp,
    show (n + 1 : ℂ) = (n + 1 : ℝ) by norm_cast, show (m : ℂ) = (m : ℝ) by norm_cast,
    mul_cpow_ofReal_nonneg m.cast_nonneg Hn, mul_inv, mul_comm]

Premises used: Nat.cast_nonneg, mul_inv, Complex.mul_cpow_ofReal_nonneg, mul_comm
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
e_a : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
⊢ ((↑(↑m : ℝ) : ℂ) ^ (↑x : ℂ))⁻¹ * (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
    ((↑(↑m : ℝ) : ℂ) ^ (↑x : ℂ))⁻¹ * ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹

Tactic:
congr
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ -(↑x : ℂ) = (↑(-1) : ℂ) * (↑x : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
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 : ℂ)
e_a₄ e_a₅ : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ)
⊢ (↑(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]

Premises used: Real.rpow_neg_one, Complex.cpow_mul_ofReal_nonneg, Complex.cpow_neg, inv_inv
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
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)))
⊢ Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))

Tactic:
obtain ⟨y, hay, hyt⟩ := exists_between ha

Premises used: exists_between
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : EReal
hay : abscissaOfAbsConv f < y
hyt : y < ⊤
⊢ y ≠ ⊤ ∧ y ≠ ⊥

Tactic:
⟨hyt.ne, ((OrderBot.bot_le _).trans_lt hay).ne'⟩

Premises used: LT.lt.ne', OrderBot.bot_le, And.intro, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : EReal
hay : abscissaOfAbsConv f < y
hyt : y < ⊤
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)))
⊢ 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'⟩
-- 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 : ℂ)
x : ℝ
m : ℕ
hm : m ≤ n + 1
⊢ F x m = 0

Tactic:
simp [F, not_lt_of_ge hm]

Premises used: not_lt_of_ge
-- 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 : ℂ)
⊢ ∀ (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]
-- 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
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)
inr₁ : ∀ (H : n + 1 < m), F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m
⊢ F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m

Tactic:
rcases lt_trichotomy m (n + 1) with H | rfl | H

Premises used: HAdd.hAdd, OfNat.ofNat, rfl, lt_trichotomy
-- 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
x : ℝ
m : ℕ
hm : m ≠ n + 1
H : m < n + 1
⊢ F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m

Tactic:
simp [Nat.not_lt_of_gt H, term, h m <| Nat.lt_succ_iff.mp H, F]

Premises used: Nat.not_lt_of_gt, Nat.lt_succ_iff, Iff.mp, LSeries.term
-- 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
x : ℝ
hm : n + 1 ≠ n + 1
⊢ F x (n + 1) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) (n + 1)

Tactic:
(hm rfl).elim

Premises used: False.elim, rfl
-- 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
x : ℝ
hm : n + 1 ≠ n + 1
⊢ F x (n + 1) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) (n + 1)

Tactic:
exact (hm rfl).elim

Premises used: False.elim, rfl
-- 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
x : ℝ
m : ℕ
hm : m ≠ n + 1
H : n + 1 < m
⊢ F x m = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m

Tactic:
simp [H, term, (n.zero_lt_succ.trans H).ne', F, cpow_mul_div_cpow_eq_div_div_cpow]

Premises used: Nat.zero_lt_succ, LT.lt.ne', _private.0.cpow_mul_div_cpow_eq_div_div_cpow, LT.lt.trans, LSeries.term
-- 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
⊢ ∀ (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]
-- 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
x : ℝ
hx : x ≥ y
⊢ Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m

Tactic:
(summable_mul_left_iff <| natCast_add_one_cpow_ne_zero n _).mpr <|
       LSeriesSummable_of_abscissaOfAbsConv_lt_re ?_

Premises used: Iff.mpr, Complex.natCast_add_one_cpow_ne_zero, LSeriesSummable_of_abscissaOfAbsConv_lt_re, summable_mul_left_iff
-- 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
x : ℝ
hx : x ≥ y
refine : abscissaOfAbsConv f < (↑(↑x : ℂ).re : EReal)
⊢ Summable (α := ℂ) fun (m : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m

Tactic:
refine (summable_mul_left_iff <| natCast_add_one_cpow_ne_zero n _).mpr <|
       LSeriesSummable_of_abscissaOfAbsConv_lt_re ?_

Premises used: Iff.mpr, Complex.natCast_add_one_cpow_ne_zero, LSeriesSummable_of_abscissaOfAbsConv_lt_re, summable_mul_left_iff
-- 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
x : ℝ
hx : x ≥ y
⊢ abscissaOfAbsConv f < (↑(↑x : ℂ).re : EReal)

Tactic:
simpa only [ofReal_re] using hay.trans_le <| EReal.coe_le_coe_iff.mpr hx

Premises used: Iff.mpr, EReal.coe_le_coe_iff, LT.lt.trans_le, Complex.ofReal_re
-- 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
⊢ ∀ {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
-- 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
x : ℝ
hx : x ≥ y
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
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ) = 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]

Premises used: tsum_mul_left, Complex.ofReal, LSeries, HAdd.hAdd, Summable.tsum_eq_add_tsum_ite, LSeries.pow_mul_term_eq, 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
x : ℝ
hx : x ≥ y
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
⊢ (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:
congr
-- 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
x : ℝ
hx : x ≥ y
e_a : ∀ (m : ℕ), (if m = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m) = F x m
⊢ 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:
ext1 m
-- 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
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)
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
⊢ (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

Premises used: HAdd.hAdd, eq_or_ne, OfNat.ofNat, rfl
-- 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
x : ℝ
hx : x ≥ y
⊢ (if n + 1 = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) (n + 1)) = F x (n + 1)

Tactic:
simp [hF₀ x le_rfl]

Premises used: le_rfl
-- 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
x : ℝ
hx : x ≥ y
m : ℕ
hm : m ≠ n + 1
⊢ (if m = n + 1 then 0 else HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * term f (↑x : ℂ) m) = F x m

Tactic:
simp [hm, hF]
-- 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
⊢ ∀ 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]
-- 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
enter : f (n + 1)
| Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))

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
rw : f (n + 1) + 0
| f (n + 1)

Tactic:
rw [← add_zero (f _)]

Premises used: add_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
enter : f (n + 1) + 0
| Tendsto (fun (x : ℝ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * LSeries f (↑x : ℂ)) atTop (nhds (f (n + 1)))

Tactic:
enter [3, 1]; rw [← add_zero (f _)]

Premises used: add_zero