awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |(↑n : ℝ) + b| ^ s = 0
⊢ 0 < (↑n : ℝ) + b
have linarith : (↑n : ℝ) + b ≤ 0 → (↑n : ℝ) + b - 0 + (-b - (↑n : ℝ)) = 0
Tactic: linarith [lt_of_abs_lt ((abs_neg b).symm ▸ Nat.lt_of_ceil_lt hn)]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |(↑n : ℝ) + b| ^ s = 0
⊢ 1 / |(↑n : ℝ) + c| ^ s = 0
have hna : 0 < (↑n : ℝ) + b
Tactic: have hna : 0 < n + b := by linarith [lt_of_abs_lt ((abs_neg b).symm ▸ Nat.lt_of_ceil_lt hn)]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |(↑n : ℝ) + b| ^ s = 0
hna : 0 < (↑n : ℝ) + b
⊢ 1 / |(↑n : ℝ) + c| ^ s = 0
have h₁ : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |(↑n : ℝ) + b| ^ s = 0
hna : 0 < (↑n : ℝ) + b
⊢ False
have h₁ : ∀ (hx : 1 / |(↑n : ℝ) + b| ^ s = 0), False
Tactic: revert hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
⊢ Tendsto (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + c| ^ s) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s) atTop
    (𝓝 1)
have refine_2 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ |(↑i : ℝ) + b| ^ s / |(↑i : ℝ) + c| ^ s) atTop (𝓝 1)
Tactic: simp_rw [Pi.div_def, div_div, mul_one_div, one_div_div]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ |(↑i : ℝ) + b| ^ s / |(↑i : ℝ) + c| ^ s) atTop (𝓝 1)
have refine_2 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)
Tactic: refine (?_ : Tendsto (fun x : ℝ ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)).comp
      tendsto_natCast_atTop_atTop
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)
have this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
Tactic: have : Tendsto (fun x : ℝ ↦ 1 + (b - c) / x) atTop (𝓝 1) := by
      simpa using tendsto_const_nhds.add ((tendsto_const_nhds (X := ℝ)).div_atTop tendsto_id)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
have refine : EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ 1 + (b - c) / x) ∘ fun (x : ℝ) ↦ id x + c) fun (x : ℝ) ↦ (x + b) / (x + c)
Tactic: refine (this.comp (tendsto_id.atTop_add (tendsto_const_nhds (x := c)))).congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ 1 + (b - c) / x) ∘ fun (x : ℝ) ↦ id x + c) fun (x : ℝ) ↦ (x + b) / (x + c)
have h₁ : ∀ (x : ℝ) (hx : -c < x), ((fun (x : ℝ) ↦ 1 + (b - c) / x) ∘ fun (x : ℝ) ↦ id x + c) x = (x + b) / (x + c)
Tactic: filter_upwards [eventually_gt_atTop (-c)] with x hx
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
x : ℝ
hx : -c < x
⊢ 0 < x + c
have linarith : x + c ≤ 0 → -c - x + (x + c - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)
have this₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
Tactic: have : Tendsto (fun x ↦ (x + b) / (x + c)) atTop (𝓝 1) := by
      refine (this.comp (tendsto_id.atTop_add (tendsto_const_nhds (x := c)))).congr' ?_
      filter_upwards [eventually_gt_atTop (-c)] with x hx
      simp [field, (by linarith : 0 < x + c).ne']
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)
have refine_2 : EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) fun (x : ℝ) ↦
  |x + b| ^ s / |x + c| ^ s
Tactic: apply (one_rpow s ▸ (continuousAt_rpow_const _ s (by simp)).tendsto.comp this).congr'
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) fun (x : ℝ) ↦
    |x + b| ^ s / |x + c| ^ s
have h₁ : ∀ (x : ℝ) (hb : -b < x) (hc : -c < x),
  ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s
Tactic: filter_upwards [eventually_gt_atTop (-b), eventually_gt_atTop (-c)] with x hb hc
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : -b < x
hc : -c < x
⊢ ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s
have hb₁ : 0 < x + b
Tactic: rw [neg_lt_iff_pos_add] at hb hc
Cleared hypotheses: hb, hc
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : -b < x
hc : -c < x
hb₁ : 0 < x + b
⊢ ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s
have hc₁ : 0 < x + c
Tactic: rw [neg_lt_iff_pos_add] at hb hc
Cleared hypotheses: hb, hc
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : 0 < x + b
hc : 0 < x + c
⊢ ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s
have h₁ : ((x + b) / (x + c)) ^ s = |x + b| ^ s / |x + c| ^ s
Tactic: rw [Function.comp_apply, div_rpow hb.le hc.le, abs_of_pos hb, abs_of_pos hc]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : 0 < x + b
hc : 0 < x + c
h₁ : ((x + b) / (x + c)) ^ s = |x + b| ^ s / |x + c| ^ s
⊢ ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s
have h₂ : (x + b) ^ s / (x + c) ^ s = |x + b| ^ s / |x + c| ^ s
Tactic: rw [Function.comp_apply, div_rpow hb.le hc.le, abs_of_pos hb, abs_of_pos hc]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : 0 < x + b
hc : 0 < x + c
h₁ : ((x + b) / (x + c)) ^ s = |x + b| ^ s / |x + c| ^ s
h₂ : (x + b) ^ s / (x + c) ^ s = |x + b| ^ s / |x + c| ^ s
⊢ ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s
have h₃ : (x + b) ^ s / (x + c) ^ s = (x + b) ^ s / |x + c| ^ s
Tactic: rw [Function.comp_apply, div_rpow hb.le hc.le, abs_of_pos hb, abs_of_pos hc]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)
x : ℝ
hb : 0 < x + b
hc : 0 < x + c
h₁ : ((x + b) / (x + c)) ^ s = |x + b| ^ s / |x + c| ^ s
h₂ : (x + b) ^ s / (x + c) ^ s = |x + b| ^ s / |x + c| ^ s
h₃ : (x + b) ^ s / (x + c) ^ s = (x + b) ^ s / |x + c| ^ s
⊢ ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) x = |x + b| ^ s / |x + c| ^ s
have h₄ : (x + b) ^ s / (x + c) ^ s = (x + b) ^ s / (x + c) ^ s
Tactic: rw [Function.comp_apply, div_rpow hb.le hc.le, abs_of_pos hb, abs_of_pos hc]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have simp_rw : ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(-(↑n : ℤ)) : ℝ) + a| ^ s) ↔
  1 < s
Tactic: simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
    Int.cast_neg, neg_neg, Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
simp_rw :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(-(↑n : ℤ)) : ℝ) + a| ^ s) ↔
    1 < s
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have simp_rw₁ : ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(-((↑(-(↑n : ℤ)) : ℝ) + a))| ^ s) ↔
  1 < s
Tactic: simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
    Int.cast_neg, neg_neg, Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
simp_rw :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(-(↑n : ℤ)) : ℝ) + a| ^ s) ↔
    1 < s
simp_rw₁ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(-((↑(-(↑n : ℤ)) : ℝ) + a))| ^ s) ↔
    1 < s
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have simp_rw₂ : ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |-(↑(-(↑n : ℤ)) : ℝ) + -a| ^ s) ↔
  1 < s
Tactic: simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
    Int.cast_neg, neg_neg, Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
simp_rw :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(-(↑n : ℤ)) : ℝ) + a| ^ s) ↔
    1 < s
simp_rw₁ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(-((↑(-(↑n : ℤ)) : ℝ) + a))| ^ s) ↔
    1 < s
simp_rw₂ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |-(↑(-(↑n : ℤ)) : ℝ) + -a| ^ s) ↔
    1 < s
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have simp_rw₃ : ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |- -(↑(↑n : ℤ) : ℝ) + -a| ^ s) ↔
  1 < s
Tactic: simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
    Int.cast_neg, neg_neg, Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
simp_rw :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(-(↑n : ℤ)) : ℝ) + a| ^ s) ↔
    1 < s
simp_rw₁ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(-((↑(-(↑n : ℤ)) : ℝ) + a))| ^ s) ↔
    1 < s
simp_rw₂ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |-(↑(-(↑n : ℤ)) : ℝ) + -a| ^ s) ↔
    1 < s
simp_rw₃ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |- -(↑(↑n : ℤ) : ℝ) + -a| ^ s) ↔
    1 < s
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have simp_rw₄ : ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + -a| ^ s) ↔
  1 < s
Tactic: simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
    Int.cast_neg, neg_neg, Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
simp_rw :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(-(↑n : ℤ)) : ℝ) + a| ^ s) ↔
    1 < s
simp_rw₁ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(-((↑(-(↑n : ℤ)) : ℝ) + a))| ^ s) ↔
    1 < s
simp_rw₂ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |-(↑(-(↑n : ℤ)) : ℝ) + -a| ^ s) ↔
    1 < s
simp_rw₃ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |- -(↑(↑n : ℤ) : ℝ) + -a| ^ s) ↔
    1 < s
simp_rw₄ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + -a| ^ s) ↔
    1 < s
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have simp_rw₅ : ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ∧ Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + -a| ^ s) ↔
  1 < s
Tactic: simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
    Int.cast_neg, neg_neg, Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
simp_rw :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(-(↑n : ℤ)) : ℝ) + a| ^ s) ↔
    1 < s
simp_rw₁ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(-((↑(-(↑n : ℤ)) : ℝ) + a))| ^ s) ↔
    1 < s
simp_rw₂ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |-(↑(-(↑n : ℤ)) : ℝ) + -a| ^ s) ↔
    1 < s
simp_rw₃ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |- -(↑(↑n : ℤ) : ℝ) + -a| ^ s) ↔
    1 < s
simp_rw₄ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + a| ^ s) ∧
      Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑(↑n : ℤ) : ℝ) + -a| ^ s) ↔
    1 < s
simp_rw₅ :
  ((Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ∧ Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + -a| ^ s) ↔
    1 < s
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have simp_rw₆ : 1 < s ∧ 1 < s ↔ 1 < s
Tactic: simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
    Int.cast_neg, neg_neg, Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
x : α
inst : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖x / HAdd.hAdd (α := α) (↑n : α) (↑k : α) ^ q‖
have simp_rw : Summable (α := ℝ) fun (n : ℕ) ↦ ‖x‖ / ‖HAdd.hAdd (α := α) (↑n : α) (↑k : α) ^ q‖
Tactic: simp_rw [norm_div]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
x : α
inst : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖x‖ / ‖HAdd.hAdd (α := α) (↑n : α) (↑k : α) ^ q‖
have h : Summable (α := ℝ) fun (x : ℕ) ↦ 1 / ‖HAdd.hAdd (α := α) (↑x : α) (↑k : α) ^ q‖
Tactic: apply Summable.const_div
-- Lean 4 proof step from Mathlib.Analysis.PSeriesComplex (goal)
Goal:
p : ℂ
⊢ (Summable (α := ℂ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℂ) (↑n : ℂ) p) ↔ 1 < p.re
have rw : (Summable (α := ℝ) fun (x : ℕ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑(x + 1) : ℂ) p‖) ↔
  Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) p.re
Tactic: rw [← Real.summable_one_div_nat_rpow, ← summable_nat_add_iff 1 (G := ℝ),
    ← summable_nat_add_iff 1 (G := ℂ), ← summable_norm_iff]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree
have pos : ∀ (h : P = 0), IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree
Tactic: by_cases h : P = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
pos :
  ∀ (h : P = 0), IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree
have neg : ∀ (h : ¬P = 0), IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree
Tactic: by_cases h : P = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : ¬P = 0
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree
have neg : IsEquivalent (E' := 𝕜) atTop
  (fun (x : 𝕜) ↦ ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) fun (x : 𝕜) ↦
  P.leadingCoeff * x ^ P.natDegree
Tactic: simp only [Polynomial.eval_eq_sum_range, sum_range_succ]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atTop ↔ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
have refine : ∀ (h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atTop), 0 < P.degree ∧ 0 ≤ P.leadingCoeff
Tactic: refine ⟨fun h => ?_, fun h => tendsto_atTop_of_leadingCoeff_nonneg P h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atTop
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
have this : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop atTop
Tactic: have : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop atTop :=
    (isEquivalent_atTop_lead P).tendsto_atTop h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atTop
this : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop atTop
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
have this₁ : 0 < P.degree ∧ 0 < P.leadingCoeff
Tactic: rw [tendsto_const_mul_pow_atTop_iff, ← pos_iff_ne_zero, natDegree_pos_iff_degree_pos] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop
have inl : ∀ (hP : 0 ≤ P.leadingCoeff), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop
Tactic: rcases le_total 0 P.leadingCoeff with hP | hP
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
inl : ∀ (hP : 0 ≤ P.leadingCoeff), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop
have inr : ∀ (hP : P.leadingCoeff ≤ 0), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atTop atTop
Tactic: rcases le_total 0 P.leadingCoeff with hP | hP
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ (IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|) ↔ P.degree ≤ 0
have refine : ∀ (h : IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|), P.degree ≤ 0
Tactic: refine ⟨fun h => ?_, fun h => ⟨|P.coeff 0|, eventually_map.mpr (Eventually.of_forall
    (forall_imp (fun _ => le_of_eq) fun x => congr_arg abs <| _root_.trans (congr_arg (eval x)
    (eq_C_of_degree_le_zero h)) eval_C))⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|
⊢ P.degree ≤ 0
have contrapose! : ∀ (h : 0 < P.degree), ¬IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atTop fun (x : 𝕜) ↦ |eval x P|
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0
have refine_1 : ∀ (h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)), P.leadingCoeff = c ∧ P.degree ≤ 0
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
refine_1 : ∀ (h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)), P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0
have refine_2 : ∀ (h : P.leadingCoeff = c ∧ P.degree ≤ 0), Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0
have this : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
Tactic: have := P.isEquivalent_atTop_lead.tendsto_nhds h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0
have pos : ∀ (hP : P.leadingCoeff = 0), P.leadingCoeff = c ∧ P.degree ≤ 0
Tactic: by_cases hP : P.leadingCoeff = 0