awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n k : ℕ
h : k ∈ range n
⊢ 0 ≤ f (u (k + 1))

Tactic:
exact h_nonneg (u (k + 1))

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n k : ℕ
h : k ∈ range n
⊢ u (k + 2) - u (k + 1) ≤ C * (u (k + 1) - u k)

Tactic:
mod_cast h_succ_diff k

Premises used: HMul.hMul, HSub.hSub, cast, LE.le, HAdd.hAdd, Eq.refl, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n k : ℕ
h : k ∈ range n
⊢ u (k + 2) - u (k + 1) ≤ C * (u (k + 1) - u k)

Tactic:
exact mod_cast h_succ_diff k
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))

Tactic:
have : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤
    C • ((u (k + 1) - u k) • f (u (k + 1))) := by
    intro k _
    rw [smul_smul]
    gcongr
    · exact h_nonneg (u (k + 1))
    exact mod_cast h_succ_diff k
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
this : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))
⊢ LE.le.{u_1} (α := M) (∑ i ∈ range n, (u (i + 2) - u (i + 1)) • f (u (i + 1)))
    (∑ i ∈ range n, C • (u (i + 1) - u i) • f (u (i + 1)))

Tactic:
sum_le_sum this

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
this : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))
h :
  HSMul.hSMul (β := M) C (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) =
    ∑ i ∈ range n, C • (u (i + 1) - u i) • f (u (i + 1))
⊢ ∑ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤
    HSMul.hSMul (β := M) C (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)))

Tactic:
convert! sum_le_sum this

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
this : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))
⊢ HSMul.hSMul (β := M) C (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) =
    ∑ i ∈ range n, C • (u (i + 1) - u i) • f (u (i + 1))

Tactic:
simp [smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
grw :
  ∑ k ∈ range (n + 1), HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k) ≤
    f 1 + HSMul.hSMul (α := ℕ) (β := M) 2 (∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 (k + 1)))
⊢ ∑ k ∈ range (n + 1), HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k) ≤
    f 1 + HSMul.hSMul (α := ℕ) (β := M) 2 (∑ k ∈ Ico 2 (HPow.hPow (α := ℕ) 2 n + 1), f k)

Tactic:
grw [← sum_condensed_le' hf n]

Premises used: Finset.sum_condensed_le'
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (n + 1), HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k) ≤
    f 1 + HSMul.hSMul (α := ℕ) (β := M) 2 (∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 (k + 1)))

Tactic:
simp [sum_range_succ', add_comm, pow_succ', mul_nsmul', sum_nsmul]

Premises used: Finset.sum_nsmul, mul_nsmul', add_comm, Finset.sum_range_succ', pow_succ'
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
rw :
  ⨆ (i : ℕ), ∑ a ∈ range (u i), f a ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ range (u 0), f k)
      (∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k))
⊢ ∑' (k : ℕ), f k ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ range (u 0), f k)
      (∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k))

Tactic:
rw [ENNReal.tsum_eq_iSup_nat' hu.tendsto_atTop]

Premises used: ENNReal.tsum_eq_iSup_nat', StrictMono.tendsto_atTop
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
refine :
  ∀ (n : ℕ),
    ∑ a ∈ range (u n), f a ≤
      HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ range (u 0), f k)
        (∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k))
⊢ ⨆ (i : ℕ), ∑ a ∈ range (u i), f a ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ range (u 0), f k)
      (∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k))

Tactic:
refine iSup_le fun n => ?_

Premises used: iSup_le
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
grw :
  HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ range (u 0), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ range (u 0), f k)
      (∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k))
⊢ ∑ a ∈ range (u n), f a ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ range (u 0), f k)
      (∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k))

Tactic:
grw [Finset.le_sum_schlomilch hf h_pos hu.monotone n]

Premises used: StrictMono.monotone, Finset.le_sum_schlomilch
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
bc :
  LE.le (α := ℝ≥0∞) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
    (∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k))
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ range (u 0), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ range (u 0), f k)
      (∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k))

Tactic:
gcongr
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n k : ℕ
⊢ HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) = (↑(u (k + 1) - u k) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
⊢ ∀ (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) = (↑(u (k + 1) - u k) : ℝ≥0∞)

Tactic:
have (k : ℕ) : (u (k + 1) - u k : ℝ≥0∞) = (u (k + 1) - (u k : ℕ) : ℕ) := by simp
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
this : ∀ (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) = (↑(u (k + 1) - u k) : ℝ≥0∞)
bc :
  LE.le (α := ℝ≥0∞) (∑ x ∈ range n, (↑(u (x + 1) - u x) : ℝ≥0∞) * f (u x))
    (∑' (k : ℕ), (↑(u (k + 1) - u k) : ℝ≥0∞) * f (u k))
⊢ LE.le (α := ℝ≥0∞) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
    (∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k))

Tactic:
simp only [nsmul_eq_mul, this]

Premises used: nsmul_eq_mul
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
this : ∀ (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) = (↑(u (k + 1) - u k) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ x ∈ range n, (↑(u (x + 1) - u x) : ℝ≥0∞) * f (u x))
    (∑' (k : ℕ), (↑(u (k + 1) - u k) : ℝ≥0∞) * f (u k))

Tactic:
apply ENNReal.sum_le_tsum

Premises used: ENNReal.sum_le_tsum
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
rw :
  ⨆ (i : ℕ), ∑ a ∈ range (HPow.hPow (α := ℕ) 2 i), f a ≤
    f 0 + ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k)
⊢ ∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k)

Tactic:
rw [ENNReal.tsum_eq_iSup_nat' (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)]

Premises used: ENNReal.tsum_eq_iSup_nat', tendsto_pow_atTop_atTop_of_one_lt, one_lt_two
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ⨆ (i : ℕ), ∑ a ∈ range (HPow.hPow (α := ℕ) 2 i), f a ≤
    f 0 + ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k)

Tactic:
iSup_le fun n => (Finset.le_sum_condensed hf n).trans ?_

Premises used: Finset.le_sum_condensed, iSup_le, LE.le.trans
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
refine :
  ∀ (n : ℕ),
    f 0 + ∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k) ≤
      f 0 + ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k)
⊢ ⨆ (i : ℕ), ∑ a ∈ range (HPow.hPow (α := ℕ) 2 i), f a ≤
    f 0 + ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k)

Tactic:
refine iSup_le fun n => (Finset.le_sum_condensed hf n).trans ?_

Premises used: Finset.le_sum_condensed, iSup_le, LE.le.trans
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
simp :
  f 0 + ∑ x ∈ range n, HPow.hPow (α := ℝ≥0∞) 2 x * f (HPow.hPow (α := ℕ) 2 x) ≤
    f 0 + ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k)
⊢ f 0 + ∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k) ≤
    f 0 + ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k)

Tactic:
simp only [nsmul_eq_mul, Nat.cast_pow, Nat.cast_two]

Premises used: nsmul_eq_mul, Nat.cast_pow, Nat.cast_two
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
grw grw₁ :
  f 0 + ∑' (x : ℕ), HPow.hPow (α := ℝ≥0∞) 2 x * f (HPow.hPow (α := ℕ) 2 x) ≤
    f 0 + ∑' (x : ℕ), HPow.hPow (α := ℝ≥0∞) 2 x * f (HPow.hPow (α := ℕ) 2 x)
⊢ f 0 + ∑ x ∈ range n, HPow.hPow (α := ℝ≥0∞) 2 x * f (HPow.hPow (α := ℕ) 2 x) ≤
    f 0 + ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k)

Tactic:
grw [ENNReal.sum_le_tsum]

Premises used: ENNReal.sum_le_tsum
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
rw :
  ⨆ (i : ℕ), ∑ a ∈ range i.succ, HSub.hSub (α := ℝ≥0∞) (↑(u (a + 1)) : ℝ≥0∞) (↑(u a) : ℝ≥0∞) * f (u a) ≤
    HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * f (u 0) +
      HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑' (k : ℕ), f k)
⊢ ∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * f (u k) ≤
    HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * f (u 0) +
      HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑' (k : ℕ), f k)

Tactic:
rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id)]

Premises used: Filter.tendsto_id, Filter.tendsto_atTop_mono, ENNReal.tsum_eq_iSup_nat', Nat.le_succ
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
⊢ ⨆ (i : ℕ), ∑ a ∈ range i.succ, HSub.hSub (α := ℝ≥0∞) (↑(u (a + 1)) : ℝ≥0∞) (↑(u a) : ℝ≥0∞) * f (u a) ≤
    HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * f (u 0) +
      HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑' (k : ℕ), f k)

Tactic:
iSup_le fun n => ?_

Premises used: iSup_le
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
refine :
  ∀ (n : ℕ),
    ∑ a ∈ range n.succ, HSub.hSub (α := ℝ≥0∞) (↑(u (a + 1)) : ℝ≥0∞) (↑(u a) : ℝ≥0∞) * f (u a) ≤
      HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * f (u 0) +
        HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑' (k : ℕ), f k)
⊢ ⨆ (i : ℕ), ∑ a ∈ range i.succ, HSub.hSub (α := ℝ≥0∞) (↑(u (a + 1)) : ℝ≥0∞) (↑(u a) : ℝ≥0∞) * f (u a) ≤
    HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * f (u 0) +
      HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑' (k : ℕ), f k)

Tactic:
refine iSup_le fun n => ?_

Premises used: iSup_le
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
grw :
  ∑ a ∈ range n.succ, HSub.hSub (α := ℝ≥0∞) (↑(u (a + 1)) : ℝ≥0∞) (↑(u a) : ℝ≥0∞) * f (u a) ≤
    HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * f (u 0) +
      HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑ x ∈ Ico (u 0 + 1) (u n + 1), f x)
⊢ ∑ a ∈ range n.succ, HSub.hSub (α := ℝ≥0∞) (↑(u (a + 1)) : ℝ≥0∞) (↑(u a) : ℝ≥0∞) * f (u a) ≤
    HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * f (u 0) +
      HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑' (k : ℕ), f k)

Tactic:
grw [← ENNReal.sum_le_tsum <| Finset.Ico (u 0 + 1) (u n + 1)]

Premises used: Finset.Ico, ENNReal.sum_le_tsum, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∑ a ∈ range n.succ, HSub.hSub (α := ℝ≥0∞) (↑(u (a + 1)) : ℝ≥0∞) (↑(u a) : ℝ≥0∞) * f (u a) ≤
    HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * f (u 0) +
      HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑ x ∈ Ico (u 0 + 1) (u n + 1), f x)

Tactic:
simpa using Finset.sum_schlomilch_le hf h_pos h_nonneg hu h_succ_diff n

Premises used: Finset.sum_schlomilch_le
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
rw :
  ⨆ (i : ℕ), ∑ a ∈ range i.succ, HPow.hPow (α := ℝ≥0∞) 2 a * f (HPow.hPow (α := ℕ) 2 a) ≤
    f 1 + HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 2 (∑' (k : ℕ), f k)
⊢ ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k) ≤ f 1 + HMul.hMul (α := ℝ≥0∞) 2 (∑' (k : ℕ), f k)

Tactic:
rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id), two_mul, ← two_nsmul]

Premises used: Filter.tendsto_id, Filter.tendsto_atTop_mono, two_mul, ENNReal.tsum_eq_iSup_nat', Nat.le_succ, two_nsmul
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ ⨆ (i : ℕ), ∑ a ∈ range i.succ, HPow.hPow (α := ℝ≥0∞) 2 a * f (HPow.hPow (α := ℕ) 2 a) ≤
    f 1 + HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 2 (∑' (k : ℕ), f k)

Tactic:
iSup_le fun n => ?_

Premises used: iSup_le
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
refine :
  ∀ (n : ℕ),
    ∑ a ∈ range n.succ, HPow.hPow (α := ℝ≥0∞) 2 a * f (HPow.hPow (α := ℕ) 2 a) ≤
      f 1 + HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 2 (∑' (k : ℕ), f k)
⊢ ⨆ (i : ℕ), ∑ a ∈ range i.succ, HPow.hPow (α := ℝ≥0∞) 2 a * f (HPow.hPow (α := ℕ) 2 a) ≤
    f 1 + HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 2 (∑' (k : ℕ), f k)

Tactic:
refine iSup_le fun n => ?_

Premises used: iSup_le
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
grw :
  ∑ a ∈ range n.succ, HPow.hPow (α := ℝ≥0∞) 2 a * f (HPow.hPow (α := ℕ) 2 a) ≤
    f 1 + HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 2 (∑ x ∈ Ico 2 (HPow.hPow (α := ℕ) 2 n + 1), f x)
⊢ ∑ a ∈ range n.succ, HPow.hPow (α := ℝ≥0∞) 2 a * f (HPow.hPow (α := ℕ) 2 a) ≤
    f 1 + HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 2 (∑' (k : ℕ), f k)

Tactic:
grw [← ENNReal.sum_le_tsum <| Finset.Ico 2 (2 ^ n + 1)]

Premises used: Finset.Ico, HPow.hPow, ENNReal.sum_le_tsum, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ a ∈ range n.succ, HPow.hPow (α := ℝ≥0∞) 2 a * f (HPow.hPow (α := ℕ) 2 a) ≤
    f 1 + HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 2 (∑ x ∈ Ico 2 (HPow.hPow (α := ℕ) 2 n + 1), f x)

Tactic:
simpa using Finset.sum_condensed_le hf n

Premises used: Finset.sum_condensed_le
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
simp :
  Eq (α := ℝ≥0∞)
      (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞ ↔
    Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
⊢ (Summable (α := ℝ≥0) fun (k : ℕ) ↦ HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0) * f (u k)) ↔ Summable f

Tactic:
simp only [← tsum_coe_ne_top_iff_summable, Ne, not_iff_not, ENNReal.coe_mul]

Premises used: not_iff_not, Ne, ENNReal.coe_mul, ENNReal.tsum_coe_ne_top_iff_summable
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
mp :
  Eq (α := ℝ≥0∞)
      (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞ →
    Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
mpr :
  Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞ →
    Eq (α := ℝ≥0∞)
      (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞
⊢ Eq (α := ℝ≥0∞)
      (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞ ↔
    Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞

Tactic:
constructor
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h :
  Eq (α := ℝ≥0∞)
    (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞
⊢ ∀ (m n : ℕ), 1 < m → m ≤ n → (↑(f n) : ℝ≥0∞) ≤ (↑(f m) : ℝ≥0∞)

Tactic:
replace hf : ∀ m n, 1 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
      ENNReal.coe_le_coe.2 (hf (zero_lt_one.trans hm) hmn)
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h :
  Eq (α := ℝ≥0∞)
    (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → (↑(f n) : ℝ≥0∞) ≤ (↑(f m) : ℝ≥0∞)
⊢ ∀ (n : ℕ), 0 ≤ (↑(f n) : ℝ≥0∞)

Tactic:
have h_nonneg : ∀ n, 0 ≤ (f n : ℝ≥0∞) := fun n =>
      ENNReal.coe_le_coe.2 (f n).2
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h :
  Eq (α := ℝ≥0∞)
    (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → (↑(f n) : ℝ≥0∞) ≤ (↑(f m) : ℝ≥0∞)
h_nonneg : ∀ (n : ℕ), 0 ≤ (↑(f n) : ℝ≥0∞)
⊢ ∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * (↑(f (u k)) : ℝ≥0∞) ≤
    HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * (↑(f (u 0)) : ℝ≥0∞) +
      HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑' (k : ℕ), (↑(f k) : ℝ≥0∞))

Tactic:
obtain hC := tsum_schlomilch_le hf h_pos h_nonneg hu_strict.monotone h_succ_diff

Premises used: StrictMono.monotone, ENNReal.tsum_schlomilch_le
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h :
  Eq (α := ℝ≥0∞)
    (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → (↑(f n) : ℝ≥0∞) ≤ (↑(f m) : ℝ≥0∞)
h_nonneg : ∀ (n : ℕ), 0 ≤ (↑(f n) : ℝ≥0∞)
hC :
  ∑' (k : ℕ), HSub.hSub (α := ℝ≥0∞) (↑(u (k + 1)) : ℝ≥0∞) (↑(u k) : ℝ≥0∞) * (↑(f (u k)) : ℝ≥0∞) ≤
    HSub.hSub (α := ℝ≥0∞) (↑(u 1) : ℝ≥0∞) (↑(u 0) : ℝ≥0∞) * (↑(f (u 0)) : ℝ≥0∞) +
      HMul.hMul (α := ℝ≥0∞) (↑C : ℝ≥0∞) (∑' (k : ℕ), (↑(f k) : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞

Tactic:
simpa [add_eq_top, mul_ne_top, mul_eq_top, hC_nonzero] using eq_top_mono hC h

Premises used: ENNReal.add_eq_top, ENNReal.mul_eq_top, ENNReal.mul_ne_top, eq_top_mono
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
⊢ ∀ (m n : ℕ), 0 < m → m ≤ n → (↑(f n) : ℝ≥0∞) ≤ (↑(f m) : ℝ≥0∞)

Tactic:
replace hf : ∀ m n, 0 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
      ENNReal.coe_le_coe.2 (hf hm hmn)
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
hf : ∀ (m n : ℕ), 0 < m → m ≤ n → (↑(f n) : ℝ≥0∞) ≤ (↑(f m) : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (∑ k ∈ range (u 0), (↑(f k) : ℝ≥0∞)) ∞

Tactic:
have : ∑ k ∈ range (u 0), (f k : ℝ≥0∞) ≠ ∞ := sum_ne_top.2 fun a _ => coe_ne_top
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
hf : ∀ (m n : ℕ), 0 < m → m ≤ n → (↑(f n) : ℝ≥0∞) ≤ (↑(f m) : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) (∑ k ∈ range (u 0), (↑(f k) : ℝ≥0∞)) ∞
⊢ Eq (α := ℝ≥0∞)
    (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞

Tactic:
simpa [h, add_eq_top, this] using le_tsum_schlomilch hf h_pos hu_strict

Premises used: ENNReal.add_eq_top, ENNReal.le_tsum_schlomilch
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ HSub.hSub (α := ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (n + 2)) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (n + 1)) ≤
    HSMul.hSMul (α := ℕ) 2
      (HSub.hSub (α := ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (n + 1)) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) n))

Tactic:
simp [pow_succ, mul_two, two_mul]

Premises used: pow_succ, two_mul, mul_two
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x

Tactic:
have h_succ_diff : SuccDiffBounded 2 (2 ^ ·) := by
    intro n
    simp [pow_succ, mul_two, two_mul]