awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
⊢ LSeriesSummable f s
have refine : ∀ (n : ℕ) (hn₀ : n ≠ 0), ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
Tactic: refine LSeriesSummable_of_le_const_mul_rpow hs ⟨C', fun n hn₀ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have inl : ∀ (hn : m ≤ n), ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
Tactic: rcases le_or_gt m n with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
inl : ∀ (hn : m ≤ n), ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have inr : ∀ (hn : n < m), ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
Tactic: rcases le_or_gt m n with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : m ≤ n
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have inl : C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
Tactic: refine (hm n hn).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : m ≤ n
⊢ C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have hn₁ : LE.le (α := ℝ) 0 (↑n : ℝ)
Tactic: have hn₀ : (0 : ℝ) ≤ n := cast_nonneg _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀_1 : n ≠ 0
hn : m ≤ n
hn₀ : LE.le (α := ℝ) 0 (↑n : ℝ)
⊢ C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have inl : ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀_1 : n ≠ 0
hn : m ≤ n
hn₀ : LE.le (α := ℝ) 0 (↑n : ℝ)
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have inl : |HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)| ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
Tactic: rw [Real.norm_eq_abs, abs_rpow_of_nonneg hn₀, abs_of_nonneg hn₀]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀_1 : n ≠ 0
hn : m ≤ n
hn₀ : LE.le (α := ℝ) 0 (↑n : ℝ)
inl : |HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)| ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have inl₁ : HPow.hPow (α := ℝ) |(↑n : ℝ)| (x - 1) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
Tactic: rw [Real.norm_eq_abs, abs_rpow_of_nonneg hn₀, abs_of_nonneg hn₀]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀_1 : n ≠ 0
hn : m ≤ n
hn₀ : LE.le (α := ℝ) 0 (↑n : ℝ)
inl : |HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)| ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
inl₁ : HPow.hPow (α := ℝ) |(↑n : ℝ)| (x - 1) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have inl₂ : HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
Tactic: rw [Real.norm_eq_abs, abs_rpow_of_nonneg hn₀, abs_of_nonneg hn₀]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have hn' : 0 < n
Tactic: have hn' : 0 < n := Nat.pos_of_ne_zero hn₀
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
⊢ ‖f n‖ ≤ C' * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
have inr : ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1) ≤ C'
Tactic: refine (div_le_iff₀ <| rpow_pos_of_pos (cast_pos.mpr hn') _).mp ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
⊢ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1) ≤ C'
have inr : Membership.mem (γ := Finset ℝ) (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))
  (‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1))
Tactic: refine (le_max' _ _ <| mem_insert_of_mem ?_).trans <| le_max_right ..
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < (↑s.re : EReal)
⊢ LSeriesSummable f s
have obtain : ∀ (y : ℝ) (hy : LSeriesSummable f (↑y : ℂ)) (hys : y < s.re), LSeriesSummable f s
Tactic: obtain ⟨y, hy, hys⟩ : ∃ a : ℝ, LSeriesSummable f a ∧ a < s.re := by
    simpa [abscissaOfAbsConv, sInf_lt_iff] using hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < (↑s.re : EReal)
⊢ ∃ x < s.re, LSeriesSummable f (↑x : ℂ)
have obtain : ∀ (x : ℝ) (hx₁ : abscissaOfAbsConv f < (↑x : EReal)) (hx₂ : (↑x : EReal) < (↑s.re : EReal)),
  ∃ x < s.re, LSeriesSummable f (↑x : ℂ)
Tactic: obtain ⟨x, hx₁, hx₂⟩ := EReal.exists_between_coe_real hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
⊢ abscissaOfAbsConv f ≤ (↑x : EReal)
have refine : ∀ (y : EReal) (hy : y ∈ lowerBounds (Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)})) (a : EReal),
  (↑x : EReal) < a → y ≤ a
Tactic: refine sInf_le_iff.mpr fun y hy ↦ le_of_forall_gt_imp_ge_of_dense fun a ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : y ∈ lowerBounds (Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)})
a : EReal
⊢ (↑x : EReal) < a → y ≤ a
have hy₁ : ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)
Tactic: replace hy : ∀ (a : ℝ), LSeriesSummable f a → y ≤ a := by simpa [mem_lowerBounds] using hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y a : EReal
hy : ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)
⊢ (↑x : EReal) < a → y ≤ a
have coe : ∀ (a₀ : ℝ), (↑x : EReal) < (↑a₀ : EReal) → y ≤ (↑a₀ : EReal)
Tactic: cases a with
  | coe a₀ => exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
  | bot => simp
  | top => simp
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y a : EReal
hy : ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)
coe : ∀ (a₀ : ℝ), (↑x : EReal) < (↑a₀ : EReal) → y ≤ (↑a₀ : EReal)
⊢ (↑x : EReal) < a → y ≤ a
have bot : (↑x : EReal) < ⊥ → y ≤ ⊥
Tactic: cases a with
  | coe a₀ => exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
  | bot => simp
  | top => simp
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f (↑y : ℂ)
y a : EReal
hy : ∀ (a : ℝ), LSeriesSummable f (↑a : ℂ) → y ≤ (↑a : EReal)
coe : ∀ (a₀ : ℝ), (↑x : EReal) < (↑a₀ : EReal) → y ≤ (↑a₀ : EReal)
bot : (↑x : EReal) < ⊥ → y ≤ ⊥
⊢ (↑x : EReal) < a → y ≤ a
have top : (↑x : EReal) < ⊤ → y ≤ ⊤
Tactic: cases a with
  | coe a₀ => exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
  | bot => simp
  | top => simp
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
⊢ abscissaOfAbsConv f ≤ ⊥
have bot : ∀ (y : EReal) (hy : ⊥ < y), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < y
Tactic: refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : ⊥ < y
⊢ ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < y
have bot : ∀ (hy : LT.lt (α := EReal) ⊥ ⊥), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < ⊥
Tactic: cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : ⊥ < y
bot : ∀ (hy : LT.lt (α := EReal) ⊥ ⊥), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < ⊥
⊢ ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < y
have bot₁ : ∀ (y : ℝ) (hy : ⊥ < (↑y : EReal)), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < (↑y : EReal)
Tactic: cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
y : EReal
hy : ⊥ < y
bot : ∀ (hy : LT.lt (α := EReal) ⊥ ⊥), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < ⊥
bot₁ : ∀ (y : ℝ) (hy : ⊥ < (↑y : EReal)), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < (↑y : EReal)
⊢ ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < y
have bot₂ : ∀ (hy : LT.lt (α := EReal) ⊥ ⊤), ∃ a ∈ Real.toEReal '' {x : ℝ | LSeriesSummable f (↑x : ℂ)}, a < ⊤
Tactic: cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : EReal
h : ∀ (y : ℝ), x < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
⊢ abscissaOfAbsConv f ≤ x
have coe : ∀ (a : ℝ) (h : ∀ (y : ℝ), (↑a : EReal) < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)), abscissaOfAbsConv f ≤ (↑a : EReal)
Tactic: cases x with
  | coe => exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h
  | top => exact le_top
  | bot =>
    refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
    cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : EReal
h : ∀ (y : ℝ), x < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
coe :
  ∀ (a : ℝ) (h : ∀ (y : ℝ), (↑a : EReal) < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)),
    abscissaOfAbsConv f ≤ (↑a : EReal)
⊢ abscissaOfAbsConv f ≤ x
have top : ∀ (h : ∀ (y : ℝ), ⊤ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)), abscissaOfAbsConv f ≤ ⊤
Tactic: cases x with
  | coe => exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h
  | top => exact le_top
  | bot =>
    refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
    cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : EReal
h : ∀ (y : ℝ), x < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)
coe :
  ∀ (a : ℝ) (h : ∀ (y : ℝ), (↑a : EReal) < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)),
    abscissaOfAbsConv f ≤ (↑a : EReal)
top : ∀ (h : ∀ (y : ℝ), ⊤ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)), abscissaOfAbsConv f ≤ ⊤
⊢ abscissaOfAbsConv f ≤ x
have bot : ∀ (h : ∀ (y : ℝ), ⊥ < (↑y : EReal) → LSeriesSummable f (↑y : ℂ)), abscissaOfAbsConv f ≤ ⊥
Tactic: cases x with
  | coe => exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h
  | top => exact le_top
  | bot =>
    refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
    cases y with
    | bot => simp at hy
    | coe y => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
    | top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ abscissaOfAbsConv f ≤ (↑x : EReal) + 1
have h₁ : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
Tactic: rw [show x = x + 1 - 1 by ring] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : ℝ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ (↑x : EReal) + 1
have by_contra! : ∀ (H : (↑x : EReal) + 1 < abscissaOfAbsConv f), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : ℝ
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
H : (↑x : EReal) + 1 < abscissaOfAbsConv f
⊢ False
have obtain : ∀ (y : ℝ) (hy₁ : (↑x : EReal) + 1 < (↑y : EReal)) (hy₂ : (↑y : EReal) < abscissaOfAbsConv f), False
Tactic: obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) x
⊢ abscissaOfAbsConv f ≤ (↑x : EReal) + 1
have h₁ : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
Tactic: rw [show x = x + 1 - 1 by ring] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : ℝ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ (↑x : EReal) + 1
have by_contra! : ∀ (H : (↑x : EReal) + 1 < abscissaOfAbsConv f), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℂ
x : ℝ
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x + 1 - 1)
H : (↑x : EReal) + 1 < abscissaOfAbsConv f
⊢ False
have obtain : ∀ (y : ℝ) (hy₁ : (↑x : EReal) + 1 < (↑y : EReal)) (hy₂ : (↑y : EReal) < abscissaOfAbsConv f), False
Tactic: obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
⊢ term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
have h₁ : ∀ (n : ℕ),
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) n = (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (hypothesis)
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ f n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have aux : term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
  (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
Tactic: have aux : term (f ·) x = fun n ↦ ↑(if n = 0 then 0 else f n / (n : ℝ) ^ x) := by
    ext n
    simp [term_def, apply_ite ((↑) : ℝ → ℂ), ofReal_cpow n.cast_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (hypothesis)
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ f n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have this : LSeriesSummable (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ)
Tactic: have := LSeriesSummable_of_abscissaOfAbsConv_lt_re (ofReal_re x ▸ h)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (hypothesis)
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
this : LSeriesSummable (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ f n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have this₁ : Summable (α := ℝ) fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x
Tactic: simp only [LSeriesSummable, aux, summable_ofReal] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
this : Summable (α := ℝ) fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ f n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have refine : Filter.EventuallyEq (β := ℝ) Filter.cofinite
  (fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x) fun (n : ℕ) ↦
  f n / HPow.hPow (α := ℝ) (↑n : ℝ) x
Tactic: refine this.congr_cofinite ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
this : Summable (α := ℝ) fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x
⊢ Filter.EventuallyEq (β := ℝ) Filter.cofinite
    (fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x) fun (n : ℕ) ↦
    f n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have h₁ : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x_1 : ℕ |
      Membership.mem (γ := Set ℕ) {0}ᶜ x_1 →
        Membership.mem (γ := Set ℕ)
          {x_2 : ℕ |
            (fun (x_3 : ℕ) ↦
                Eq (α := ℝ) ((fun (x_4 : ℕ) ↦ if x_4 = 0 then 0 else f x_4 / HPow.hPow (α := ℝ) (↑x_4 : ℝ) x) x_3)
                  ((fun (n : ℕ) ↦ f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) x_3))
              x_2}
          x_1}
    a
Tactic: filter_upwards [(Set.finite_singleton 0).compl_mem_cofinite] with n hn
    using if_neg (by simpa using hn)