awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℕ
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) ↔ 1 < p

Tactic:
simp only [one_div, Real.summable_nat_pow_inv]

Premises used: Real.summable_nat_pow_inv, one_div
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℕ
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) ↔ 1 < p

Tactic:
⟨fun h ↦ summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective),
    fun h ↦ .of_nat_of_neg (summable_one_div_nat_pow.mpr h)
      (((summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n ↦ ?_)⟩

Premises used: Iff.mpr, Summable.of_nat_of_neg, HDiv.hDiv, Summable.mul_left, HPow.hPow, Summable.comp_injective, Iff.intro, Iff.mp, Summable.congr, Real.summable_one_div_nat_pow, Nat.cast_injective, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℕ
refine :
  ∀ (h : 1 < p) (n : ℕ),
    1 / HPow.hPow (α := ℝ) (-1) p * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) = 1 / HPow.hPow (α := ℝ) (↑(-(↑n : ℤ)) : ℝ) p
⊢ (Summable (α := ℝ) fun (n : ℤ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) ↔ 1 < p

Tactic:
refine ⟨fun h ↦ summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective),
    fun h ↦ .of_nat_of_neg (summable_one_div_nat_pow.mpr h)
      (((summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n ↦ ?_)⟩
-- Module: Mathlib.Analysis.PSeries
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)
rw₅ 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

Tactic:
rw [Int.cast_neg, Int.cast_natCast, neg_eq_neg_one_mul (n : ℝ), mul_pow, mul_one_div, div_div]

Premises used: Int.cast_neg, Int.cast_natCast, Nat.cast, mul_one_div, neg_eq_neg_one_mul, div_div, mul_pow
-- Module: Mathlib.Analysis.PSeries
Goal:
b : ℝ
hb : 1 < b
hf₁ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)
hf₂ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(-(↑n : ℤ)) : ℝ)| (-b)
⊢ Summable (α := ℝ) fun (n : ℤ) ↦ HPow.hPow (α := ℝ) |(↑n : ℝ)| (-b)

Tactic:
apply Summable.of_nat_of_neg

Premises used: Summable.of_nat_of_neg
-- Module: Mathlib.Analysis.PSeries
Goal:
b : ℝ
hb : 1 < b
hf₂ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(-(↑n : ℤ)) : ℝ)| (-b)

Tactic:
simp_rw [Int.cast_neg, abs_neg]

Premises used: Int.cast_neg, abs_neg
-- Module: Mathlib.Analysis.PSeries
Goal:
b : ℝ
hb : 1 < b
hf₂ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(-(↑n : ℤ)) : ℝ)| (-b)

Tactic:
on_goal 2 => simp_rw [Int.cast_neg, abs_neg]

Premises used: Int.cast_neg, abs_neg
-- Module: Mathlib.Analysis.PSeries
Goal:
b : ℝ
hb : 1 < b
hf₁ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-b)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)

Tactic:
simp_rw [Int.cast_natCast, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]

Premises used: Int.cast_natCast, Nat.cast_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.PSeries
Goal:
b : ℝ
hb : 1 < b
hf₁ : -b < -1
hf₂ hf₃ hf₄ hf₅ : 1 < b
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-b)

Tactic:
rwa [summable_nat_rpow, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, Real.summable_nat_rpow
-- Module: Mathlib.Analysis.PSeries
Goal:
b : ℝ
hb : 1 < b
hf₂ : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-b)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| (-b)

Tactic:
simp_rw [Int.cast_natCast, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]

Premises used: Int.cast_natCast, Nat.cast_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.PSeries
Goal:
b : ℝ
hb : 1 < b
hf₂ : -b < -1
hf₃ hf₄ hf₅ hf₆ : 1 < b
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-b)

Tactic:
rwa [summable_nat_rpow, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, Real.summable_nat_rpow
-- Module: Mathlib.Analysis.PSeries
Goal:
⊢ ¬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)
-- Module: Mathlib.Analysis.PSeries
Goal:
this : ¬Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 1)⁻¹
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦ (↑n : ℝ)⁻¹

Tactic:
simpa
-- Module: Mathlib.Analysis.PSeries
Goal:
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
simpa only [inv_eq_one_div] using not_summable_natCast_inv

Premises used: inv_eq_one_div, Real.not_summable_natCast_inv
-- Module: Mathlib.Analysis.PSeries
Goal:
rw : ¬Summable (α := ℝ) fun (i : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
rw₁ : ∀ (n : ℕ), 0 ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) atTop atTop

Tactic:
rw [← not_summable_iff_tendsto_nat_atTop_of_nonneg]

Premises used: not_summable_iff_tendsto_nat_atTop_of_nonneg
-- Module: Mathlib.Analysis.PSeries
Goal:
⊢ ¬Summable (α := ℝ) fun (i : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
exact_mod_cast mt (_root_.summable_nat_add_iff 1).1 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:
i : ℕ
⊢ 0 ≤ 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Analysis.PSeries
Goal:
⊢ ∀ (n : ℕ), 0 ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
exact fun i => by positivity
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
⊢ (Summable (α := ℝ≥0) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ≥0) (↑n : ℝ≥0) p)⁻¹) ↔ 1 < p

Tactic:
simp [← NNReal.summable_coe]

Premises used: NNReal.summable_coe
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
⊢ (Summable (α := ℝ≥0) fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0) (↑n : ℝ≥0) p) ↔ p < -1

Tactic:
simp [← NNReal.summable_coe]

Premises used: NNReal.summable_coe
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
⊢ (Summable (α := ℝ≥0) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0) (↑n : ℝ≥0) p) ↔ 1 < p

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
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 : α)⁻¹

Tactic:
Nat.le_induction ?_ ?_ n h

Premises used: Nat.le_induction
-- Module: Mathlib.Analysis.PSeries
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 : α)⁻¹
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) : α)⁻¹
⊢ ∑ i ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹

Tactic:
refine Nat.le_induction ?_ ?_ n h
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
hk : k ≠ 0
h : k ≤ n
⊢ ∑ i ∈ Ioc k k, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑k : α)⁻¹

Tactic:
simp only [Ioc_self, sum_empty, sub_self, le_refl]

Premises used: le_refl, sub_self, Finset.Ioc_self, Finset.sum_empty
-- Module: Mathlib.Analysis.PSeries
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 : α)⁻¹
refine_2 :
  ∑ k ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑k : α) 2)⁻¹ + (HPow.hPow (α := α) (β := ℕ) (↑(n + 1) : α) 2)⁻¹ ≤
    HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹
⊢ ∑ i ∈ Ioc k (n + 1), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹ ≤ HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹

Tactic:
rw [sum_Ioc_succ_top hn]

Premises used: Finset.sum_Ioc_succ_top
-- Module: Mathlib.Analysis.PSeries
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 : α)⁻¹
refine_2 :
  HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ + (HPow.hPow (α := α) (β := ℕ) (↑(n + 1) : α) 2)⁻¹ ≤
    HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹
⊢ ∑ k ∈ Ioc k n, (HPow.hPow (α := α) (β := ℕ) (↑k : α) 2)⁻¹ + (HPow.hPow (α := α) (β := ℕ) (↑(n + 1) : α) 2)⁻¹ ≤
    HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹

Tactic:
grw [IH]
-- Module: Mathlib.Analysis.PSeries
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 : α)⁻¹
refine_2 :
  HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑n : α) 1) 2)⁻¹ ≤
    (↑k : α)⁻¹ - (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹
⊢ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ + (HPow.hPow (α := α) (β := ℕ) (↑(n + 1) : α) 2)⁻¹ ≤
    HSub.hSub (α := α) (↑k : α)⁻¹ (↑(n + 1) : α)⁻¹

Tactic:
push_cast
-- Module: Mathlib.Analysis.PSeries
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 : α)⁻¹
⊢ LT.lt.{u_1} (α := α) 0 (↑n : α)

Tactic:
simpa using hk.bot_lt.trans_le hn

Premises used: LT.lt.trans_le, Ne.bot_lt
-- Module: Mathlib.Analysis.PSeries
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 : α)⁻¹
⊢ LT.lt.{u_1} (α := α) 0 (↑n : α)

Tactic:
have A : 0 < (n : α) := by simpa using hk.bot_lt.trans_le hn
-- Module: Mathlib.Analysis.PSeries
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 : α)
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 : α))
⊢ HSub.hSub (α := α) (↑k : α)⁻¹ (↑n : α)⁻¹ + (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑n : α) 1) 2)⁻¹ ≤
    (↑k : α)⁻¹ - (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹

Tactic:
field_simp
-- Module: Mathlib.Analysis.PSeries
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 : α)
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
⊢ 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:
linarith
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
h : Ioo k n ⊆ Ioc k (max (k + 1) n)
hf : ∀ i ∈ Ioc k (max (k + 1) n), i ∉ Ioo k n → 0 ≤ (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹
⊢ LE.le.{u_1} (α := α) (∑ i ∈ Ioo k n, (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹)
    (∑ i ∈ Ioc k (max (k + 1) n), (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹)

Tactic:
apply sum_le_sum_of_subset_of_nonneg

Premises used: Finset.sum_le_sum_of_subset_of_nonneg
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n x : ℕ
hx : x ∈ Ioo k n
⊢ k < x ∧ x < n

Tactic:
simp only [mem_Ioo] at hx

Premises used: Finset.mem_Ioo
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n x : ℕ
hx : k < x ∧ x < n
⊢ x ∈ Ioc k (max (k + 1) n)

Tactic:
simp only [hx, hx.2.le, mem_Ioc, le_max_iff, or_true, and_self_iff]

Premises used: LT.lt.le, And.right, and_self_iff, Finset.mem_Ioc, le_max_iff, or_true
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n i : ℕ
_hi : i ∈ Ioc k (max (k + 1) n)
_hident : i ∉ Ioo k n
⊢ 0 ≤ (HPow.hPow (α := α) (β := ℕ) (↑i : α) 2)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.PSeries
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)⁻¹
hab : k + 1 < max (k + 1) n + 1
⊢ ∑ 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)⁻¹

Tactic:
rw [← Icc_add_one_left_eq_Ioc, ← Ico_add_one_right_eq_Icc, sum_eq_sum_Ico_succ_bot]

Premises used: Finset.Icc_add_one_left_eq_Ioc, Finset.Ico_add_one_right_eq_Icc, Finset.sum_eq_sum_Ico_succ_bot
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ k + 1 < max (k + 1) n + 1

Tactic:
Nat.succ_lt_succ ((Nat.lt_succ_self k).trans_le (le_max_left _ _))

Premises used: Nat.succ_lt_succ, Nat.lt_succ_self, LT.lt.trans_le, le_max_left
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ k + 1 < max (k + 1) n + 1

Tactic:
exact Nat.succ_lt_succ ((Nat.lt_succ_self k).trans_le (le_max_left _ _))

Premises used: Nat.succ_lt_succ, Nat.lt_succ_self, LT.lt.trans_le, le_max_left
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
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)⁻¹
⊢ (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 [Ico_add_one_right_eq_Icc, Icc_add_one_left_eq_Ioc]

Premises used: Finset.Icc_add_one_left_eq_Ioc, Finset.Ico_add_one_right_eq_Icc
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
norm_cast norm_cast₁ norm_cast₂ 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) : α)⁻¹)
⊢ (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:
norm_cast
-- Module: Mathlib.Analysis.PSeries
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)⁻¹

Tactic:
add_le_add le_rfl ((sum_Ioc_inv_sq_le_sub ?_ (le_max_left _ _)).trans ?_)

Premises used: le_rfl, add_le_add, sum_Ioc_inv_sq_le_sub, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
refine_1 : k.succ ≠ 0
refine_2 : HSub.hSub (α := α) (↑k.succ : α)⁻¹ (↑(max k.succ n) : α)⁻¹ ≤ (HAdd.hAdd (α := α) (↑k : α) 1)⁻¹
⊢ (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)⁻¹

Tactic:
refine add_le_add le_rfl ((sum_Ioc_inv_sq_le_sub ?_ (le_max_left _ _)).trans ?_)

Premises used: le_rfl, add_le_add, sum_Ioc_inv_sq_le_sub, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ k.succ ≠ 0

Tactic:
simp only [Ne, Nat.succ_ne_zero, not_false_iff]

Premises used: Ne, Nat.succ_ne_zero, not_false_iff
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ HSub.hSub (α := α) (↑k.succ : α)⁻¹ (↑(max k.succ n) : α)⁻¹ ≤ (HAdd.hAdd (α := α) (↑k : α) 1)⁻¹

Tactic:
simp only [Nat.cast_succ, sub_le_self_iff, inv_nonneg, Nat.cast_nonneg]

Premises used: Nat.cast_succ, Nat.cast_nonneg, inv_nonneg, sub_le_self_iff
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ 1 ≤ HAdd.hAdd (α := α) (↑k : α) 1

Tactic:
simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]

Premises used: Nat.cast_nonneg, le_add_iff_nonneg_left
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ 1 ≤ HAdd.hAdd (α := α) (↑k : α) 1

Tactic:
have A : (1 : α) ≤ k + 1 := by simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
A : 1 ≤ HAdd.hAdd (α := α) (↑k : α) 1
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
⊢ (HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2)⁻¹ + (HAdd.hAdd (α := α) (↑k : α) 1)⁻¹ ≤
    1 / HAdd.hAdd (α := α) (↑k : α) 1 + 1 / HAdd.hAdd (α := α) (↑k : α) 1

Tactic:
simp_rw [← one_div]

Premises used: one_div
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
A : 1 ≤ HAdd.hAdd (α := α) (↑k : α) 1
bc : HAdd.hAdd (α := α) (↑k : α) 1 ≤ HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2
⊢ 1 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2 + 1 / HAdd.hAdd (α := α) (↑k : α) 1 ≤
    1 / HAdd.hAdd (α := α) (↑k : α) 1 + 1 / HAdd.hAdd (α := α) (↑k : α) 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
A : 1 ≤ HAdd.hAdd (α := α) (↑k : α) 1
⊢ HAdd.hAdd (α := α) (↑k : α) 1 ≤ HPow.hPow (β := ℕ) (HAdd.hAdd (α := α) (↑k : α) 1) 2

Tactic:
simpa using pow_right_mono₀ A one_le_two

Premises used: pow_right_mono₀, one_le_two
-- Module: Mathlib.Analysis.PSeries
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
k n : ℕ
⊢ 1 / HAdd.hAdd (α := α) (↑k : α) 1 + 1 / HAdd.hAdd (α := α) (↑k : α) 1 = 2 / HAdd.hAdd (α := α) (↑k : α) 1

Tactic:
ring
-- Module: Mathlib.Analysis.PSeries
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
⊢ NeZero m

Tactic:
have : NeZero m := ⟨hm⟩
-- Module: Mathlib.Analysis.PSeries
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
rw :
  ¬Summable (α := ℝ) fun (n : ℕ) ↦
      indicator {n : ℕ | (↑n : ZMod m) = k} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (n + 1)
⊢ ¬Summable (α := ℝ) (indicator {n : ℕ | (↑n : ZMod m) = k} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
rw [← summable_nat_add_iff 1]

Premises used: summable_nat_add_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
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:
simp only [indicator_apply, mem_setOf_eq, cast_add, cast_one]

Premises used: Set.indicator_apply, Set.mem_setOf_eq, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.PSeries
Goal:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ∀ (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]
-- 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
simp_rw :
  ¬Summable (α := ℝ) fun (n : ℕ) ↦
      indicator {n : ℕ | (↑n : ZMod m) = k - 1} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) n
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦
      indicator {n : ℕ | (↑n : ZMod m) = k} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (n + 1)

Tactic:
simp_rw [indicator_apply, mem_setOf, cast_add, cast_one, ← eq_sub_iff_add_eq, ← h]

Premises used: Set.indicator_apply, eq_sub_iff_add_eq, Set.mem_setOf, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.PSeries
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
hd : LT.lt (α := ℝ) 0 (↑(n₁ + 1) : ℝ)
⊢ HDiv.hDiv (α := ℝ) 1 (↑(n₂ + 1) : ℝ) ≤ HDiv.hDiv (α := ℝ) 1 (↑(n₁ + 1) : ℝ)

Tactic:
gcongr