awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.PSeries
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h :
  ∀ (n : ℕ),
    indicator {n : ℕ | (↑n : ZMod m) = k - 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) n =
      if (↑n : ZMod m) = k - 1 then 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 else 0
rw : ¬Summable (α := ℝ) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦
      indicator {n : ℕ | (↑n : ZMod m) = k - 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) n

Tactic:
rw [summable_indicator_mod_iff (fun n₁ n₂ h ↦ by gcongr) (k - 1)]

Premises used: HSub.hSub, OfNat.ofNat, summable_indicator_mod_iff
-- Module: Mathlib.Analysis.PSeries
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h :
  ∀ (n : ℕ),
    indicator {n : ℕ | (↑n : ZMod m) = k - 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) n =
      if (↑n : ZMod m) = k - 1 then 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 else 0
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
mt (summable_nat_add_iff (f := fun n : ℕ ↦ 1 / (n : ℝ)) 1).mp not_summable_one_div_natCast

Premises used: summable_nat_add_iff, mt, Real.not_summable_one_div_natCast, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h :
  ∀ (n : ℕ),
    indicator {n : ℕ | (↑n : ZMod m) = k - 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) n =
      if (↑n : ZMod m) = k - 1 then 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 else 0
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
exact mt (summable_nat_add_iff (f := fun n : ℕ ↦ 1 / (n : ℝ)) 1).mp not_summable_one_div_natCast

Premises used: summable_nat_add_iff, mt, Real.not_summable_one_div_natCast, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
a s : ℝ
this :
  ∀ (b c : ℝ),
    (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s) → Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + c| ^ s
simp_rw :
  (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s
simp_rw₁ :
  (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |HAdd.hAdd (α := ℝ) (↑n : ℝ) 0| ^ s) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s
simp_rw₂ :
  (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) |(↑n : ℝ)| s) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s

Tactic:
simp_rw [← summable_one_div_nat_rpow, Iff.intro (this a 0) (this 0 a), add_zero, Nat.abs_cast]

Premises used: Nat.abs_cast, Real.summable_one_div_nat_rpow, Iff.intro, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
a s : ℝ
suffices :
  ∀ (b c : ℝ),
    (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s) → Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + c| ^ s
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s

Tactic:
suffices ∀ (b c : ℝ), Summable (fun n : ℕ ↦ 1 / |n + b| ^ s) →
      Summable (fun n : ℕ ↦ 1 / |n + c| ^ s) by
    simp_rw [← summable_one_div_nat_rpow, Iff.intro (this a 0) (this 0 a), add_zero, Nat.abs_cast]
-- Module: Mathlib.Analysis.PSeries
Goal:
a s : ℝ
⊢ ∀ (b c : ℝ),
    (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s) → Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + c| ^ s

Tactic:
fun b c h ↦ summable_of_isBigO_nat h (isBigO_of_div_tendsto_nhds ?_ 1 ?_)

Premises used: Asymptotics.isBigO_of_div_tendsto_nhds, OfNat.ofNat, summable_of_isBigO_nat
-- Module: Mathlib.Analysis.PSeries
Goal:
a s : ℝ
refine_1 :
  ∀ (b c : ℝ) (h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s),
    ∀ᶠ (x : ℕ) in atTop, 1 / |(↑x : ℝ) + b| ^ s = 0 → 1 / |(↑x : ℝ) + c| ^ s = 0
refine_2 :
  ∀ (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)
⊢ ∀ (b c : ℝ),
    (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s) → Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + c| ^ s

Tactic:
refine fun b c h ↦ summable_of_isBigO_nat h (isBigO_of_div_tendsto_nhds ?_ 1 ?_)

Premises used: Asymptotics.isBigO_of_div_tendsto_nhds, OfNat.ofNat, summable_of_isBigO_nat
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
h₁ : ∀ (n : ℕ) (hn : ⌈|b|⌉₊ < n) (hx : 1 / |(↑n : ℝ) + b| ^ s = 0), 1 / |(↑n : ℝ) + c| ^ s = 0
⊢ ∀ᶠ (x : ℕ) in atTop, 1 / |(↑x : ℝ) + b| ^ s = 0 → 1 / |(↑x : ℝ) + c| ^ s = 0

Tactic:
filter_upwards [eventually_gt_atTop (Nat.ceil |b|)] with n hn hx

Premises used: abs, Nat.ceil, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hx : 1 / |(↑n : ℝ) + b| ^ s = 0
linarith : (↑n : ℝ) + b ≤ 0 → (↑n : ℝ) + b - 0 + (-b - (↑n : ℝ)) = 0
⊢ 0 < (↑n : ℝ) + b

Tactic:
linarith [lt_of_abs_lt ((abs_neg b).symm ▸ Nat.lt_of_ceil_lt hn)]

Premises used: lt_of_abs_lt
-- Module: Mathlib.Analysis.PSeries
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

Tactic:
have hna : 0 < n + b := by linarith [lt_of_abs_lt ((abs_neg b).symm ▸ Nat.lt_of_ceil_lt hn)]
-- Module: Mathlib.Analysis.PSeries
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
h₁ : False
⊢ 1 / |(↑n : ℝ) + c| ^ s = 0

Tactic:
exfalso
-- Module: Mathlib.Analysis.PSeries
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
h₁ : ∀ (hx : 1 / |(↑n : ℝ) + b| ^ s = 0), False
⊢ False

Tactic:
revert hx
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
n : ℕ
hn : ⌈|b|⌉₊ < n
hna : 0 < (↑n : ℝ) + b
⊢ ∀ (hx : 1 / |(↑n : ℝ) + b| ^ s = 0), False

Tactic:
positivity
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
refine_2 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ |(↑i : ℝ) + b| ^ s / |(↑i : ℝ) + c| ^ s) atTop (𝓝 1)
⊢ Tendsto (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + c| ^ s) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s) atTop
    (𝓝 1)

Tactic:
simp_rw [Pi.div_def, div_div, mul_one_div, one_div_div]

Premises used: Pi.div_def, mul_one_div, div_div, one_div_div
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ |(↑i : ℝ) + b| ^ s / |(↑i : ℝ) + c| ^ s) atTop (𝓝 1)

Tactic:
(?_ : Tendsto (fun x : ℝ ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)).comp
      tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
refine_2 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ |(↑i : ℝ) + b| ^ s / |(↑i : ℝ) + c| ^ s) atTop (𝓝 1)

Tactic:
refine (?_ : Tendsto (fun x : ℝ ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)).comp
      tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)

Tactic:
simpa using tendsto_const_nhds.add ((tendsto_const_nhds (X := ℝ)).div_atTop tendsto_id)

Premises used: Filter.Tendsto.div_atTop, Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
⊢ 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)
-- Module: Mathlib.Analysis.PSeries
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)

Tactic:
(this.comp (tendsto_id.atTop_add (tendsto_const_nhds (x := c)))).congr' ?_

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.atTop_add, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
refine :
  EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ 1 + (b - c) / x) ∘ fun (x : ℝ) ↦ id x + c) fun (x : ℝ) ↦ (x + b) / (x + c)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + b) / (x + c)) atTop (𝓝 1)

Tactic:
refine (this.comp (tendsto_id.atTop_add (tendsto_const_nhds (x := c)))).congr' ?_

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.atTop_add, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.PSeries
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 + (b - c) / x) atTop (𝓝 1)
h₁ : ∀ (x : ℝ) (hx : -c < x), ((fun (x : ℝ) ↦ 1 + (b - c) / x) ∘ fun (x : ℝ) ↦ id x + c) x = (x + b) / (x + c)
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ 1 + (b - c) / x) ∘ fun (x : ℝ) ↦ id x + c) fun (x : ℝ) ↦ (x + b) / (x + c)

Tactic:
filter_upwards [eventually_gt_atTop (-c)] with x hx

Premises used: Neg.neg, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.PSeries
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
linarith : x + c ≤ 0 → -c - x + (x + c - 0) = 0
⊢ 0 < x + c

Tactic:
linarith
-- Module: Mathlib.Analysis.PSeries
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
⊢ ((fun (x : ℝ) ↦ 1 + (b - c) / x) ∘ fun (x : ℝ) ↦ id x + c) x = (x + b) / (x + c)

Tactic:
simp [field, (by linarith : 0 < x + c).ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.PSeries
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)

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']
-- Module: Mathlib.Analysis.PSeries
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)
⊢ Ne (α := ℝ) 1 0 ∨ 0 ≤ s

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
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)
refine_2 :
  EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) fun (x : ℝ) ↦
    |x + b| ^ s / |x + c| ^ s
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)

Tactic:
apply (one_rpow s ▸ (continuousAt_rpow_const _ s (by simp)).tendsto.comp this).congr'
-- Module: Mathlib.Analysis.PSeries
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)
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
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ s) ∘ fun (x : ℝ) ↦ (x + b) / (x + c)) fun (x : ℝ) ↦
    |x + b| ^ s / |x + c| ^ s

Tactic:
filter_upwards [eventually_gt_atTop (-b), eventually_gt_atTop (-c)] with x hb hc

Premises used: Neg.neg, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.PSeries
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
⊢ 0 < x + b

Tactic:
rw [neg_lt_iff_pos_add] at hb hc

Premises used: neg_lt_iff_pos_add
-- Module: Mathlib.Analysis.PSeries
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
⊢ 0 < x + c

Tactic:
rw [neg_lt_iff_pos_add] at hb hc

Premises used: neg_lt_iff_pos_add
-- Module: Mathlib.Analysis.PSeries
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
h₄ 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

Tactic:
rw [Function.comp_apply, div_rpow hb.le hc.le, abs_of_pos hb, abs_of_pos hc]

Premises used: LT.lt.le, Real.div_rpow, Function.comp_apply, abs_of_pos
-- Module: Mathlib.Analysis.PSeries
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
simp_rw₆ : 1 < s ∧ 1 < s ↔ 1 < 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]

Premises used: Int.cast_neg, Int.cast_natCast, abs_neg, Real.summable_one_div_nat_add_rpow, and_self, neg_add, neg_neg, summable_int_iff_summable_nat_and_neg, HAdd.hAdd
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
x : α
inst : RCLike α
q k : ℕ
hq : 1 < q
simp_rw : Summable (α := ℝ) fun (n : ℕ) ↦ ‖x‖ / ‖HAdd.hAdd (α := α) (↑n : α) (↑k : α) ^ q‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖x / HAdd.hAdd (α := α) (↑n : α) (↑k : α) ^ q‖

Tactic:
simp_rw [norm_div]

Premises used: norm_div
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
x : α
inst : RCLike α
q k : ℕ
hq : 1 < q
h : Summable (α := ℝ) fun (x : ℕ) ↦ 1 / ‖HAdd.hAdd (α := α) (↑x : α) (↑k : α) ^ q‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖x‖ / ‖HAdd.hAdd (α := α) (↑n : α) (↑k : α) ^ q‖

Tactic:
apply Summable.const_div

Premises used: Summable.const_div
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
x : α
inst : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ 1 / ‖HAdd.hAdd (α := α) (↑x : α) (↑k : α) ^ q‖

Tactic:
simpa [hq, Nat.cast_add, one_div, norm_inv, norm_pow, RCLike.norm_natCast,
    Real.summable_nat_pow_inv, iff_true]
      using summable_nat_add_iff (f := fun x => ‖1 / (x ^ q : α)‖) k

Premises used: summable_nat_add_iff, norm_pow, iff_true, Real.summable_nat_pow_inv, norm_inv, Nat.cast_add, RCLike.norm_natCast, one_div
-- Module: Mathlib.Analysis.PSeriesComplex
Goal:
p : ℂ
rw :
  (Summable (α := ℝ) fun (x : ℕ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑(x + 1) : ℂ) p‖) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) p.re
⊢ (Summable (α := ℂ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℂ) (↑n : ℂ) p) ↔ 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]

Premises used: summable_nat_add_iff, Real.summable_one_div_nat_rpow, summable_norm_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeriesComplex
Goal:
p : ℂ
⊢ (Summable (α := ℝ) fun (x : ℕ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑(x + 1) : ℂ) p‖) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) p.re

Tactic:
simp only [norm_div, norm_one, ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos
    (Nat.cast_pos.mpr <| Nat.succ_pos _)]

Premises used: Iff.mpr, Nat.cast_pos, NormOneClass.norm_one, norm_div, Nat.succ_pos, Complex.ofReal_natCast, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
hP : P ≠ 0
⊢ ∀ᶠ (x : 𝕜) in atTop, ¬P.IsRoot x

Tactic:
atTop_le_cofinite <| (finite_setOf_isRoot hP).compl_mem_cofinite

Premises used: Filter.Eventually, Set.Finite.compl_mem_cofinite, Polynomial.finite_setOf_isRoot, Filter.atTop_le_cofinite
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
hP : P ≠ 0
⊢ ∀ᶠ (x : 𝕜) in atBot, ¬P.IsRoot x

Tactic:
atBot_le_cofinite <| (finite_setOf_isRoot hP).compl_mem_cofinite

Premises used: Filter.Eventually, Filter.atBot_le_cofinite, Set.Finite.compl_mem_cofinite, Polynomial.finite_setOf_isRoot
-- Module: Mathlib.Analysis.Polynomial.Basic
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
neg :
  ∀ (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

Tactic:
by_cases h : P = 0
-- Module: Mathlib.Analysis.Polynomial.Basic
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

Tactic:
simp [h, IsEquivalent.refl]

Premises used: Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : ¬P = 0
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
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
simp only [Polynomial.eval_eq_sum_range, sum_range_succ]

Premises used: Polynomial.eval_eq_sum_range, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Polynomial.Basic
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 : 𝕜) ↦ ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) fun (x : 𝕜) ↦
    P.leadingCoeff * x ^ P.natDegree

Tactic:
IsLittleO.add_isEquivalent
        (IsLittleO.sum fun i hi =>
          IsLittleO.const_mul_left
            ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
              isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
            _)
        IsEquivalent.refl

Premises used: Asymptotics.IsLittleO.sum, Asymptotics.IsLittleO.const_mul_left, Finset.mem_range, Polynomial.coeff, Asymptotics.IsEquivalent.refl, Iff.mp, Asymptotics.IsLittleO.const_mul_right, Asymptotics.IsLittleO.add_isEquivalent, Polynomial.leadingCoeff_eq_zero, Asymptotics.isLittleO_pow_pow_atTop_of_lt
-- Module: Mathlib.Analysis.Polynomial.Basic
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 : 𝕜) ↦ ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) fun (x : 𝕜) ↦
    P.leadingCoeff * x ^ P.natDegree

Tactic:
exact
      IsLittleO.add_isEquivalent
        (IsLittleO.sum fun i hi =>
          IsLittleO.const_mul_left
            ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
              isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
            _)
        IsEquivalent.refl

Premises used: Asymptotics.IsLittleO.sum, Asymptotics.IsLittleO.const_mul_left, Finset.mem_range, Asymptotics.IsEquivalent.refl, Iff.mp, Asymptotics.IsLittleO.const_mul_right, Asymptotics.IsLittleO.add_isEquivalent, Polynomial.leadingCoeff_eq_zero, Asymptotics.isLittleO_pow_pow_atTop_of_lt
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
hnng : 0 ≤ P.leadingCoeff
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atTop

Tactic:
P.isEquivalent_atTop_lead.symm.tendsto_atTop <|
    tendsto_const_mul_pow_atTop (natDegree_pos_iff_degree_pos.2 hdeg).ne' <|
      hnng.lt_of_ne' <| leadingCoeff_ne_zero.mpr <| ne_zero_of_degree_gt hdeg

Premises used: Iff.mpr, Polynomial.isEquivalent_atTop_lead, Polynomial.ne_zero_of_degree_gt, Filter.tendsto_const_mul_pow_atTop, LT.lt.ne', Polynomial.leadingCoeff_ne_zero, Asymptotics.IsEquivalent.tendsto_atTop, Polynomial.natDegree_pos_iff_degree_pos, LE.le.lt_of_ne', Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
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

Tactic:
⟨fun h => ?_, fun h => tendsto_atTop_of_leadingCoeff_nonneg P h.1 h.2⟩

Premises used: And.right, And.left, Polynomial.tendsto_atTop_of_leadingCoeff_nonneg, Iff.intro
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
refine : ∀ (h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P) atTop atTop), 0 < P.degree ∧ 0 ≤ P.leadingCoeff
⊢ 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⟩
-- Module: Mathlib.Analysis.Polynomial.Basic
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
⊢ 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
-- Module: Mathlib.Analysis.Polynomial.Basic
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

Tactic:
rw [tendsto_const_mul_pow_atTop_iff, ← pos_iff_ne_zero, natDegree_pos_iff_degree_pos] at this

Premises used: Filter.tendsto_const_mul_pow_atTop_iff, Polynomial.natDegree_pos_iff_degree_pos, pos_iff_ne_zero