awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
p : ℕ
h : 1 < p
n : ℕ
rw : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑(↑n : ℤ) : ℝ)) p
rw₁ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (-(↑n : ℝ)) p
rw₂ : 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HMul.hMul (α := ℝ) (-1) (↑n : ℝ) ^ p
rw₃ :
  1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) =
    1 / (HPow.hPow (α := ℝ) (-1) p * HPow.hPow (α := ℝ) (↑n : ℝ) p)
rw₄ :
  1 / HPow.hPow (α := ℝ) (-1) p / HPow.hPow (α := ℝ) (↑n : ℝ) p =
    1 / (HPow.hPow (α := ℝ) (-1) p * HPow.hPow (α := ℝ) (↑n : ℝ) p)
⊢ 1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (↑(-(↑n : ℤ)) : ℝ) p
have rw₅ : 1 / (HPow.hPow (α := ℝ) (-1) p * HPow.hPow (α := ℝ) (↑n : ℝ) p) =
  1 / (HPow.hPow (α := ℝ) (-1) p * HPow.hPow (α := ℝ) (↑n : ℝ) p)
Tactic: rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ Summable (α := ℝ) fun (n : ℤ) ↦ HPow.hPow (α := ℝ) |(↑n : ℝ)| (-b)
have hf₁ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)
Tactic: apply Summable.of_nat_of_neg
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
b : ℝ
hb : 1 < b
hf₁ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)
⊢ Summable (α := ℝ) fun (n : ℤ) ↦ HPow.hPow (α := ℝ) |(↑n : ℝ)| (-b)
have hf₂ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(-(↑n : ℤ)) : ℝ)| (-b)
Tactic: apply Summable.of_nat_of_neg
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(-(↑n : ℤ)) : ℝ)| (-b)
have hf₂ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)
Tactic: simp_rw [Int.cast_neg, abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(-(↑n : ℤ)) : ℝ)| (-b)
have hf₂ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)
Tactic: on_goal 2 => simp_rw [Int.cast_neg, abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)
have hf₁ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-b)
Tactic: simp_rw [Int.cast_natCast, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-b)
have hf₁ : -b < -1
Tactic: rwa [summable_nat_rpow, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)
have hf₂ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-b)
Tactic: simp_rw [Int.cast_natCast, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
b : ℝ
hb : 1 < b
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-b)
have hf₂ : -b < -1
Tactic: rwa [summable_nat_rpow, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦ (↑n : ℝ)⁻¹
have this : ¬Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 1)⁻¹
Tactic: have : ¬Summable (fun n => ((n : ℝ) ^ 1)⁻¹ : ℕ → ℝ) :=
    mt (summable_nat_pow_inv (p := 1)).1 (lt_irrefl 1)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) atTop atTop
have rw : ¬Summable (α := ℝ) fun (i : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: rw [← not_summable_iff_tendsto_nat_atTop_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
rw : ¬Summable (α := ℝ) fun (i : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) atTop atTop
have rw₁ : ∀ (n : ℕ), 0 ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rw [← not_summable_iff_tendsto_nat_atTop_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
hk : k ≠ 0
h : k ≤ n
⊢ ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹
have refine_1 : ∑ i ∈ Ioc k k, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑k : α)⁻¹
Tactic: refine Nat.le_induction ?_ ?_ n h
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
hk : k ≠ 0
h : k ≤ n
refine_1 : ∑ i ∈ Ioc k k, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑k : α)⁻¹
⊢ ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹
have refine_2 : ∀ (n : ℕ) (hmn : k ≤ n),
  ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ →
    ∑ i ∈ Ioc k (n + 1), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹
Tactic: refine Nat.le_induction ?_ ?_ n h
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n_1 : ℕ
hk : k ≠ 0
h : k ≤ n_1
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹
⊢ ∑ i ∈ Ioc k (n + 1), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹
have refine_2 : ∑ k ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑k : α) 2)⁻¹ + (HPow.hPow (α := α) (β := ℕ) (↑(n + 1) : α) 2)⁻¹ ≤
  HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹
Tactic: rw [sum_Ioc_succ_top hn]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n_1 : ℕ
hk : k ≠ 0
h : k ≤ n_1
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹
⊢ ∑ k ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑k : α) 2)⁻¹ + (HPow.hPow (α := α) (β := ℕ) (↑(n + 1) : α) 2)⁻¹ ≤
    HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹
have refine_2 : HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ + (HPow.hPow (α := α) (β := ℕ) (↑(n + 1) : α) 2)⁻¹ ≤
  HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹
Tactic: grw [IH]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n_1 : ℕ
hk : k ≠ 0
h : k ≤ n_1
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹
⊢ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ + (HPow.hPow (α := α) (β := ℕ) (↑(n + 1) : α) 2)⁻¹ ≤
    HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹
have refine_2 : HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑n : α) 1) 2)⁻¹ ≤
  (↑k : α)⁻¹ - (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n_1 : ℕ
hk : k ≠ 0
h : k ≤ n_1
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹
⊢ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑n : α) 1) 2)⁻¹ ≤
    (↑k : α)⁻¹ - (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹
have A : LT.lt.{u_1} (α := α) 0 (↑n : α)
Tactic: have A : 0 < (n : α) := by simpa using hk.bot_lt.trans_le hn
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n_1 : ℕ
hk : k ≠ 0
h : k ≤ n_1
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹
A : LT.lt.{u_1} (α := α) 0 (↑n : α)
⊢ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑n : α) 1) 2)⁻¹ ≤
    (↑k : α)⁻¹ - (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹
have refine_2 : HSub.hSub (α := α) (↑n : α) (↑k : α) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑n : α) 1) 2 +
    HMul.hMul (α := α) (↑k : α) (↑n : α) ≤
  (↑n : α) * HAdd.hAdd (α := α) (↑n : α) 1 * (HAdd.hAdd (α := α) (↑n : α) 1 - (↑k : α))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n_1 : ℕ
hk : k ≠ 0
h : k ≤ n_1
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹
A : LT.lt.{u_1} (α := α) 0 (↑n : α)
⊢ HSub.hSub (α := α) (↑n : α) (↑k : α) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑n : α) 1) 2 +
      HMul.hMul (α := α) (↑k : α) (↑n : α) ≤
    (↑n : α) * HAdd.hAdd (α := α) (↑n : α) 1 * (HAdd.hAdd (α := α) (↑n : α) 1 - (↑k : α))
have linarith : (↑n : α) * HAdd.hAdd (α := α) (↑n : α) 1 * (HAdd.hAdd (α := α) (↑n : α) 1 - (↑k : α)) <
    HSub.hSub (α := α) (↑n : α) (↑k : α) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑n : α) 1) 2 +
      HMul.hMul (α := α) (↑k : α) (↑n : α) →
  HSub.hSub (α := α) 0 (↑k : α) +
      ((↑n : α) * HAdd.hAdd (α := α) (↑n : α) 1 * (HAdd.hAdd (α := α) (↑n : α) 1 - (↑k : α)) -
        (HSub.hSub (α := α) (↑n : α) (↑k : α) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑n : α) 1) 2 +
          HMul.hMul (α := α) (↑k : α) (↑n : α))) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ LE.le.{u_1} (α := α) (∑ i ∈ Ioo k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹)
    (∑ i ∈ Ioc k (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹)
have h : Ioo k n ⊆ Ioc k (max (k + 1) n)
Tactic: apply sum_le_sum_of_subset_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
h : Ioo k n ⊆ Ioc k (max (k + 1) n)
⊢ LE.le.{u_1} (α := α) (∑ i ∈ Ioo k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹)
    (∑ i ∈ Ioc k (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹)
have hf : ∀ i ∈ Ioc k (max (k + 1) n), i ∉ Ioo k n → 0 ≤ (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹
Tactic: apply sum_le_sum_of_subset_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n x : ℕ
hx : x ∈ Ioo k n
⊢ x ∈ Ioc k (max (k + 1) n)
have hx₁ : k < x ∧ x < n
Tactic: simp only [mem_Ioo] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ ∑ i ∈ Ioc k (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ +
      ∑ i ∈ Ioc k.succ (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹
have rw : (HPow.hPow (α := α) (β := ℕ) (↑(k + 1) : α) 2)⁻¹ +
    ∑ k ∈ Ico (k + 1 + 1) (max (k + 1) n + 1), (HPow.hPow (α := α) (β := ℕ) (↑k : α) 2)⁻¹ ≤
  (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ +
    ∑ i ∈ Ioc k.succ (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹
Tactic: rw [← Icc_add_one_left_eq_Ioc, ← Ico_add_one_right_eq_Icc, sum_eq_sum_Ico_succ_bot]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
rw :
  (HPow.hPow (α := α) (β := ℕ) (↑(k + 1) : α) 2)⁻¹ +
      ∑ k ∈ Ico (k + 1 + 1) (max (k + 1) n + 1), (HPow.hPow (α := α) (β := ℕ) (↑k : α) 2)⁻¹ ≤
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ +
      ∑ i ∈ Ioc k.succ (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹
⊢ ∑ i ∈ Ioc k (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ +
      ∑ i ∈ Ioc k.succ (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹
have hab : k + 1 < max (k + 1) n + 1
Tactic: rw [← Icc_add_one_left_eq_Ioc, ← Ico_add_one_right_eq_Icc, sum_eq_sum_Ico_succ_bot]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ (HPow.hPow (α := α) (β := ℕ) (↑(k + 1) : α) 2)⁻¹ +
      ∑ k ∈ Ico (k + 1 + 1) (max (k + 1) n + 1), (HPow.hPow (α := α) (β := ℕ) (↑k : α) 2)⁻¹ ≤
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ +
      ∑ i ∈ Ioc k.succ (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹
have rw : (HPow.hPow (α := α) (β := ℕ) (↑(k + 1) : α) 2)⁻¹ +
    ∑ k ∈ Ioc (k + 1) (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑k : α) 2)⁻¹ ≤
  (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ +
    ∑ i ∈ Ioc k.succ (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹
Tactic: rw [Ico_add_one_right_eq_Icc, Icc_add_one_left_eq_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ (HPow.hPow (α := α) (β := ℕ) (↑(k + 1) : α) 2)⁻¹ +
      ∑ k ∈ Ioc (k + 1) (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑k : α) 2)⁻¹ ≤
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ +
      ∑ i ∈ Ioc k.succ (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹
have norm_cast : HAdd.hAdd (α := α) (↑(HPow.hPow (β := ℕ) (k + 1) 2) : α)⁻¹
    (∑ x ∈ Ioc (k + 1) (max (k + 1) n), (↑(HPow.hPow (β := ℕ) x 2) : α)⁻¹) ≤
  HAdd.hAdd (α := α) (↑(HPow.hPow (β := ℕ) (k + 1) 2) : α)⁻¹
    (∑ x ∈ Ioc (k + 1) (max (k + 1) n), (↑(HPow.hPow (β := ℕ) x 2) : α)⁻¹)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ +
      ∑ i ∈ Ioc k.succ (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ + (HAdd.hAdd (α := α) (↑k : α) 1)⁻¹
have refine_1 : k.succ ≠ 0
Tactic: refine add_le_add le_rfl ((sum_Ioc_inv_sq_le_sub ?_ (le_max_left _ _)).trans ?_)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
refine_1 : k.succ ≠ 0
⊢ (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ +
      ∑ i ∈ Ioc k.succ (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ + (HAdd.hAdd (α := α) (↑k : α) 1)⁻¹
have refine_2 : HSub.hSub (α := α) (↑k.succ : α)⁻¹ (↑(max k.succ n) : α)⁻¹ ≤ (HAdd.hAdd (α := α) (↑k : α) 1)⁻¹
Tactic: refine add_le_add le_rfl ((sum_Ioc_inv_sq_le_sub ?_ (le_max_left _ _)).trans ?_)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ + (HAdd.hAdd (α := α) (↑k : α) 1)⁻¹ ≤
    1 / HAdd.hAdd (α := α) (↑k : α) 1 + 1 / HAdd.hAdd (α := α) (↑k : α) 1
have A : 1 ≤ HAdd.hAdd (α := α) (↑k : α) 1
Tactic: have A : (1 : α) ≤ k + 1 := by simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
A : 1 ≤ HAdd.hAdd (α := α) (↑k : α) 1
⊢ (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ + (HAdd.hAdd (α := α) (↑k : α) 1)⁻¹ ≤
    1 / HAdd.hAdd (α := α) (↑k : α) 1 + 1 / HAdd.hAdd (α := α) (↑k : α) 1
have simp_rw : 1 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2 + 1 / HAdd.hAdd (α := α) (↑k : α) 1 ≤
  1 / HAdd.hAdd (α := α) (↑k : α) 1 + 1 / HAdd.hAdd (α := α) (↑k : α) 1
Tactic: simp_rw [← one_div]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
A : 1 ≤ HAdd.hAdd (α := α) (↑k : α) 1
⊢ 1 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2 + 1 / HAdd.hAdd (α := α) (↑k : α) 1 ≤
    1 / HAdd.hAdd (α := α) (↑k : α) 1 + 1 / HAdd.hAdd (α := α) (↑k : α) 1
have bc : HAdd.hAdd (α := α) (↑k : α) 1 ≤ HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
⊢ ¬Summable (α := ℝ) (indicator {n : ℕ | (↑n : ZMod m) = k} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have this : NeZero m
Tactic: have : NeZero m := ⟨hm⟩
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ¬Summable (α := ℝ) (indicator {n : ℕ | (↑n : ZMod m) = k} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw : ¬Summable (α := ℝ) fun (n : ℕ) ↦
    indicator {n : ℕ | (↑n : ZMod m) = k} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (n + 1)
Tactic: rw [← summable_nat_add_iff 1]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦
      indicator {n : ℕ | (↑n : ZMod m) = k} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (n + 1)
have 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
Tactic: have h (n : ℕ) : {n : ℕ | (n : ZMod m) = k - 1}.indicator (fun n : ℕ ↦ (1 / (n + 1 :) : ℝ)) n =
      if (n : ZMod m) = k - 1 then (1 / (n + 1) : ℝ) else (0 : ℝ) := by
    simp only [indicator_apply, mem_setOf_eq, cast_add, cast_one]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 : ℕ) ↦
      indicator {n : ℕ | (↑n : ZMod m) = k} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (n + 1)
have simp_rw : ¬Summable (α := ℝ) fun (n : ℕ) ↦
    indicator {n : ℕ | (↑n : ZMod m) = k - 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) n
Tactic: simp_rw [indicator_apply, mem_setOf, cast_add, cast_one, ← eq_sub_iff_add_eq, ← h]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h_1 :
  ∀ (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
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ HDiv.hDiv (α := ℝ) 1 (↑(n₂ + 1) : ℝ) ≤ HDiv.hDiv (α := ℝ) 1 (↑(n₁ + 1) : ℝ)
have hc : LE.le (α := ℝ) 0 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h_1 :
  ∀ (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
n₁ n₂ : ℕ
h : n₁ ≤ n₂
hc : LE.le (α := ℝ) 0 1
⊢ HDiv.hDiv (α := ℝ) 1 (↑(n₂ + 1) : ℝ) ≤ HDiv.hDiv (α := ℝ) 1 (↑(n₁ + 1) : ℝ)
have hd : LT.lt (α := ℝ) 0 (↑(n₁ + 1) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 : ℕ) ↦
      indicator {n : ℕ | (↑n : ZMod m) = k - 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) n
have rw : ¬Summable (α := ℝ) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)
Tactic: rw [summable_indicator_mod_iff (fun n₁ n₂ h ↦ by gcongr) (k - 1)]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
this :
  ∀ (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
have simp_rw : (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔
  Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s
Tactic: simp_rw [← summable_one_div_nat_rpow, Iff.intro (this a 0) (this 0 a), add_zero, Nat.abs_cast]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have simp_rw₁ : (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |HAdd.hAdd (α := ℝ) (↑n : ℝ) 0| ^ s) ↔
  Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s
Tactic: simp_rw [← summable_one_div_nat_rpow, Iff.intro (this a 0) (this 0 a), add_zero, Nat.abs_cast]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have simp_rw₂ : (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) |(↑n : ℝ)| s) ↔
  Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s
Tactic: simp_rw [← summable_one_div_nat_rpow, Iff.intro (this a 0) (this 0 a), add_zero, Nat.abs_cast]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + a| ^ s) ↔ 1 < s
have suffices : ∀ (b c : ℝ),
  (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s) → Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + c| ^ 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]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s : ℝ
⊢ ∀ (b c : ℝ),
    (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s) → Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + c| ^ s
have 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
Tactic: refine fun b c h ↦ summable_of_isBigO_nat h (isBigO_of_div_tendsto_nhds ?_ 1 ?_)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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
⊢ ∀ (b c : ℝ),
    (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s) → Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + c| ^ s
have 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)
Tactic: refine fun b c h ↦ summable_of_isBigO_nat h (isBigO_of_div_tendsto_nhds ?_ 1 ?_)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
a s b c : ℝ
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / |(↑n : ℝ) + b| ^ s
⊢ ∀ᶠ (x : ℕ) in atTop, 1 / |(↑x : ℝ) + b| ^ s = 0 → 1 / |(↑x : ℝ) + c| ^ s = 0
have h₁ : ∀ (n : ℕ) (hn : ⌈|b|⌉₊ < n) (hx : 1 / |(↑n : ℝ) + b| ^ s = 0), 1 / |(↑n : ℝ) + c| ^ s = 0
Tactic: filter_upwards [eventually_gt_atTop (Nat.ceil |b|)] with n hn hx