awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
zero : LE.le.{u_1} (α := M) (∑ k ∈ range 0, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u 0 + 1), f k)
⊢ LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
have succ : ∀ (n : ℕ)
  (ihn : LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)),
  LE.le.{u_1} (α := M) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u (k + 1)))
    (∑ k ∈ Ico (u 0 + 1) (u (n + 1) + 1), f k)
Tactic: induction n with
  | zero => simp
  | succ n ihn =>
    suffices (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      exacts [add_le_add ihn this,
        (add_le_add_left (hu n.zero_le) _ : u 0 + 1 ≤ u n + 1),
        add_le_add_left (hu n.le_succ) _]
    have : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k := fun k hk =>
      hf (Nat.lt_of_le_of_lt (Nat.succ_le_of_lt (h_pos n)) <| (Nat.lt_succ_of_le le_rfl).trans_le
        (mem_Ico.mp hk).1) (Nat.le_of_lt_succ <| (mem_Ico.mp hk).2)
    convert! sum_le_sum this
    simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 : ℕ
⊢ LE.le.{u_1} (α := M) (∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 (k + 1)))
    (∑ k ∈ Ico 2 (HPow.hPow (α := ℕ) 2 n + 1), f k)
have h : ∀ x ∈ range n,
  HPow.hPow (α := ℕ) 2 x • f (HPow.hPow (α := ℕ) 2 (x + 1)) =
    (HPow.hPow (α := ℕ) 2 (x + 1) - HPow.hPow (α := ℕ) 2 x) • f (HPow.hPow (α := ℕ) 2 (x + 1))
Tactic: convert!
    sum_schlomilch_le' hf (fun n => pow_pos zero_lt_two n)
      (fun m n hm => pow_right_mono₀ one_le_two hm) n using 2
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 + 1), (u (k + 1) - u k) • f (u k) ≤
    (u 1 - u 0) • f (u 0) + HSMul.hSMul (β := M) C (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
have rw : (u (HAdd.hAdd (α := ℕ) 0 1) - u 0) • f (u 0) + ∑ k ∈ range n, (u (k + 1 + 1) - u (k + 1)) • f (u (k + 1)) ≤
  (u 1 - u 0) • f (u 0) + HSMul.hSMul (β := M) C (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
Tactic: rw [sum_range_succ', add_comm]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 : ℕ
⊢ (u (HAdd.hAdd (α := ℕ) 0 1) - u 0) • f (u 0) + ∑ k ∈ range n, (u (k + 1 + 1) - u (k + 1)) • f (u (k + 1)) ≤
    (u 1 - u 0) • f (u 0) + HSMul.hSMul (β := M) C (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
have bc : ∑ k ∈ range n, (u (k + 1 + 1) - u (k + 1)) • f (u (k + 1)) ≤ HSMul.hSMul (β := M) C (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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)) ≤
    HSMul.hSMul (β := M) C (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)))
⊢ ∑ k ∈ range n, (u (k + 1 + 1) - u (k + 1)) • f (u (k + 1)) ≤
    HSMul.hSMul (β := M) C (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
have refine : LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
Tactic: refine this.trans (nsmul_le_nsmul_right ?_ _)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 + 1 + 1) - u (k + 1)) • f (u (k + 1)) ≤
    HSMul.hSMul (β := M) C (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
have bc : ∑ 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: suffices ∑ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤
  C • ∑ k ∈ range n, ((u (k + 1) - u k) • f (u (k + 1))) by
    refine this.trans (nsmul_le_nsmul_right ?_ _)
    exact sum_schlomilch_le' hf h_pos hu n
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))
have rw : (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ (C * (u (k + 1) - u k)) • f (u (k + 1))
Tactic: rw [smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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)) • f (u (k + 1)) ≤ (C * (u (k + 1) - u k)) • f (u (k + 1))
have hb : 0 ≤ f (u (k + 1))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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
hb : 0 ≤ f (u (k + 1))
⊢ (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ (C * (u (k + 1) - u k)) • f (u (k + 1))
have ha : u (k + 2) - u (k + 1) ≤ C * (u (k + 1) - u k)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
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)) ≤
    HSMul.hSMul (β := M) C (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)))
have this : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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))
⊢ ∑ 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)))
have 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))
Tactic: convert! sum_le_sum this
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 ∈ Ico 2 (HPow.hPow (α := ℕ) 2 n + 1), f k)
have 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)))
Tactic: grw [← sum_condensed_le' hf n]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
⊢ ∑' (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))
have 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))
Tactic: rw [ENNReal.tsum_eq_iSup_nat' hu.tendsto_atTop]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
⊢ ⨆ (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))
have 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))
Tactic: refine iSup_le fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 : ℕ
⊢ ∑ 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))
have 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))
Tactic: grw [Finset.le_sum_schlomilch hf h_pos hu.monotone n]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 : ℕ
⊢ 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))
have 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))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
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 : ℕ
⊢ 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))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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∞) (∑ 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))
have 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))
Tactic: simp only [nsmul_eq_mul, this]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k)
have rw : ⨆ (i : ℕ), ∑ a ∈ range (HPow.hPow (α := ℕ) 2 i), f a ≤
  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)]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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)
have 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)
Tactic: refine iSup_le fun n => (Finset.le_sum_condensed hf n).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
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)
have 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)
Tactic: simp only [nsmul_eq_mul, Nat.cast_pow, Nat.cast_two]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ 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)
have 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)
Tactic: grw [ENNReal.sum_le_tsum]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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
⊢ ∑' (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)
have 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)
Tactic: rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id)]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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)
have 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)
Tactic: refine iSup_le fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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∞) (∑' (k : ℕ), f k)
have 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)
Tactic: grw [← ENNReal.sum_le_tsum <| Finset.Ico (u 0 + 1) (u n + 1)]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ ∑' (k : ℕ), HPow.hPow (α := ℝ≥0∞) 2 k * f (HPow.hPow (α := ℕ) 2 k) ≤ f 1 + HMul.hMul (α := ℝ≥0∞) 2 (∑' (k : ℕ), f k)
have 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)
Tactic: rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id), two_mul, ← two_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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)
have 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)
Tactic: refine iSup_le fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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 (∑' (k : ℕ), f k)
have 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)
Tactic: grw [← ENNReal.sum_le_tsum <| Finset.Ico 2 (2 ^ n + 1)]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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
⊢ (Summable (α := ℝ≥0) fun (k : ℕ) ↦ HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0) * f (u k)) ↔ Summable f
have 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∞)) ∞
Tactic: simp only [← tsum_coe_ne_top_iff_summable, Ne, not_iff_not, ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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
⊢ Eq (α := ℝ≥0∞)
      (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞ ↔
    Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
have 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∞)) ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
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∞)) ∞
⊢ Eq (α := ℝ≥0∞)
      (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞ ↔
    Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
have 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∞)) ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
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∞)) ∞
⊢ Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
have hf₁ : ∀ (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)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
have h_nonneg : ∀ (n : ℕ), 0 ≤ (↑(f n) : ℝ≥0∞)
Tactic: have h_nonneg : ∀ n, 0 ≤ (f n : ℝ≥0∞) := fun n =>
      ENNReal.coe_le_coe.2 (f n).2
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) (∑' (b : ℕ), (↑(f b) : ℝ≥0∞)) ∞
have 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∞))
Tactic: obtain hC := tsum_schlomilch_le hf h_pos h_nonneg hu_strict.monotone h_succ_diff
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
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∞)) ∞
⊢ Eq (α := ℝ≥0∞)
    (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞
have hf₁ : ∀ (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)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞)
    (∑' (b : ℕ), (↑(HSub.hSub (α := ℝ≥0) (↑(u (b + 1)) : ℝ≥0) (↑(u b) : ℝ≥0)) : ℝ≥0∞) * (↑(f (u b)) : ℝ≥0∞)) ∞
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable (α := ℝ≥0) fun (k : ℕ) ↦ HPow.hPow (α := ℝ≥0) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
have h_succ_diff : 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]