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 : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
succ : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u (n + 1)), f k) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k))

Tactic:
suffices (∑ k ∈ Ico (u n) (u (n + 1)), f k) ≤ (u (n + 1) - u n) • f (u n) by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      · exact add_le_add ihn this
      exacts [hu n.zero_le, hu n.le_succ]
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
⊢ ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)

Tactic:
have : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n) := fun k hk =>
      hf (Nat.succ_le_of_lt (h_pos n)) (mem_Ico.mp hk).1
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)
⊢ LE.le.{u_1} (α := M) (∑ i ∈ Ico (u n) (u (n + 1)), f i) (∑ i ∈ Ico (u n) (u (n + 1)), f (u n))

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 : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)
h : (u (n + 1) - u n) • f (u n) = ∑ i ∈ Ico (u n) (u (n + 1)), f (u n)
⊢ ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)

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 : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)
⊢ (u (n + 1) - u n) • f (u n) = ∑ i ∈ Ico (u n) (u (n + 1)), f (u n)

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
zero : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u 0), f k) (∑ k ∈ range 0, (u (k + 1) - u k) • f (u k))
succ :
  ∀ (n : ℕ) (ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))),
    LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u (n + 1)), f k) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k))
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))

Tactic:
induction n with
  | zero => simp
  | succ n ihn =>
    suffices (∑ k ∈ Ico (u n) (u (n + 1)), f k) ≤ (u (n + 1) - u n) • f (u n) by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      · exact add_le_add ihn this
      exacts [hu n.zero_le, hu n.le_succ]
    have : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n) := fun k hk =>
      hf (Nat.succ_le_of_lt (h_pos n)) (mem_Ico.mp hk).1
    convert! sum_le_sum this
    simp
-- 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 : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (HPow.hPow (α := ℕ) (β := ℕ) 2 0) (HPow.hPow (α := ℕ) 2 n), f k)
    (∑ k ∈ range n, (HPow.hPow (α := ℕ) 2 (k + 1) - HPow.hPow (α := ℕ) 2 k) • f (HPow.hPow (α := ℕ) 2 k))

Tactic:
le_sum_schlomilch' hf (fun n => pow_pos zero_lt_two n)
      (fun m n hm => pow_right_mono₀ one_le_two hm) n

Premises used: pow_pos, Finset.le_sum_schlomilch', pow_right_mono₀
-- 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 : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
h :
  ∀ x ∈ range n,
    HPow.hPow (α := ℕ) 2 x • f (HPow.hPow (α := ℕ) 2 x) =
      (HPow.hPow (α := ℕ) 2 (x + 1) - HPow.hPow (α := ℕ) 2 x) • f (HPow.hPow (α := ℕ) 2 x)
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k)
    (∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k))

Tactic:
convert!
    le_sum_schlomilch' hf (fun n => pow_pos zero_lt_two n)
      (fun m n hm => pow_right_mono₀ one_le_two hm) n using 2

Premises used: pow_pos, Finset.le_sum_schlomilch', pow_right_mono₀
-- 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 : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n x : ℕ
h : x ∈ range n
⊢ HPow.hPow (α := ℕ) 2 x • f (HPow.hPow (α := ℕ) 2 x) =
    (HPow.hPow (α := ℕ) 2 (x + 1) - HPow.hPow (α := ℕ) 2 x) • f (HPow.hPow (α := ℕ) 2 x)

Tactic:
simp [pow_succ, mul_two]

Premises used: pow_succ, mul_two
-- Module: Mathlib.Analysis.PSeries
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
grw : ∑ k ∈ range (u n), f k ≤ HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ Ico (u 0) (u n), f k)
grw₁ grw₂ :
  HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ Ico (u 0) (u n), f k) ≤
    HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ Ico (u 0) (u n), f k)
⊢ ∑ k ∈ range (u n), f k ≤ HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))

Tactic:
grw [← le_sum_schlomilch' hf h_pos hu n, ← sum_range_add_sum_Ico _ (hu n.zero_le)]

Premises used: Nat.zero_le, Finset.sum_range_add_sum_Ico, Finset.le_sum_schlomilch'
-- 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 : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
grw : ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₁ :
  HAdd.hAdd (α := M) (∑ k ∈ range 1, f k) (∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k) ≤
    f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₂ :
  ∑ x ∈ range 0, f x + f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₃ : 0 + f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₄ grw₅ : f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
⊢ ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k)

Tactic:
grw [← le_sum_condensed' hf n, ← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ,
    sum_range_zero, zero_add]

Premises used: Finset.sum_range_add_sum_Ico, Finset.le_sum_condensed', Nat.one_le_two_pow, Finset.sum_range_zero, zero_add, Finset.sum_range_succ
-- Module: Mathlib.Analysis.PSeries
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
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
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 : ℕ
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)
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
rw :
  ∑ x ∈ range n, (u (x + 1) - u x) • f (u (x + 1)) + (u (n + 1) - u n) • f (u (n + 1)) ≤
    HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0 + 1) (u n + 1), f i) (∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f i)
n₁ : ℕ
hmn : u 0 + 1 ≤ u n + 1
hnk : u n + 1 ≤ u (n + 1) + 1
⊢ 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:
rw [sum_range_succ, ← sum_Ico_consecutive]

Premises used: Finset.sum_Ico_consecutive, Finset.sum_range_succ
-- Module: Mathlib.Analysis.PSeries
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 : ℕ
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)
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
⊢ ∑ x ∈ range n, (u (x + 1) - u x) • f (u (x + 1)) + (u (n + 1) - u n) • f (u (n + 1)) ≤
    HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0 + 1) (u n + 1), f i) (∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f i)

Tactic:
add_le_add ihn this

Premises used: add_le_add
-- Module: Mathlib.Analysis.PSeries
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 : ℕ
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)
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
⊢ u 0 + 1 ≤ u n + 1

Tactic:
(add_le_add_left (hu n.zero_le) _ : u 0 + 1 ≤ u n + 1)

Premises used: Nat.zero_le, add_le_add_left
-- Module: Mathlib.Analysis.PSeries
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 : ℕ
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)
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
⊢ u n + 1 ≤ u (n + 1) + 1

Tactic:
add_le_add_left (hu n.le_succ) _

Premises used: add_le_add_left, Nat.le_succ
-- Module: Mathlib.Analysis.PSeries
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 : ℕ
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)
succ : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 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:
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) _]
-- Module: Mathlib.Analysis.PSeries
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 : ℕ
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)
⊢ ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k

Tactic:
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)
-- Module: Mathlib.Analysis.PSeries
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 : ℕ
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)
this : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k
⊢ LE.le.{u_1} (α := M) (∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1))) (∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f i)

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 : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
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)
this : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k
h : (u (n + 1) - u n) • f (u (n + 1)) = ∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1))
⊢ (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k

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 : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
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)
this : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k
⊢ (u (n + 1) - u n) • f (u (n + 1)) = ∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1))

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
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)
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)
⊢ 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:
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
-- 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 : ℕ
⊢ LE.le.{u_1} (α := M)
    (∑ k ∈ range n, (HPow.hPow (α := ℕ) 2 (k + 1) - HPow.hPow (α := ℕ) 2 k) • f (HPow.hPow (α := ℕ) 2 (k + 1)))
    (∑ k ∈ Ico (HPow.hPow (α := ℕ) (β := ℕ) 2 0 + 1) (HPow.hPow (α := ℕ) 2 n + 1), f k)

Tactic:
sum_schlomilch_le' hf (fun n => pow_pos zero_lt_two n)
      (fun m n hm => pow_right_mono₀ one_le_two hm) n

Premises used: pow_pos, pow_right_mono₀, Finset.sum_schlomilch_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 : ℕ
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))
⊢ 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)

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

Premises used: pow_pos, pow_right_mono₀, Finset.sum_schlomilch_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 x : ℕ
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:
simp [pow_succ, mul_two]

Premises used: pow_succ, mul_two
-- 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 : ℕ
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)
⊢ ∑ 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)

Tactic:
rw [sum_range_succ', add_comm]

Premises used: add_comm, Finset.sum_range_succ'
-- 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 : ℕ
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)
⊢ (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:
gcongr
-- 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)) ≤
    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)

Tactic:
this.trans (nsmul_le_nsmul_right ?_ _)

Premises used: nsmul_le_nsmul_right, LE.le.trans
-- 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)) ≤
    HSMul.hSMul (β := M) C (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)))
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)
⊢ ∑ 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:
refine this.trans (nsmul_le_nsmul_right ?_ _)

Premises used: nsmul_le_nsmul_right, LE.le.trans
-- 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)) ≤
    HSMul.hSMul (β := M) C (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)))
⊢ 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:
sum_schlomilch_le' hf h_pos hu n

Premises used: Finset.sum_schlomilch_le'
-- 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)) ≤
    HSMul.hSMul (β := M) C (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)))
⊢ 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:
exact sum_schlomilch_le' hf h_pos hu n

Premises used: Finset.sum_schlomilch_le'
-- 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 : ℕ
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)))
⊢ ∑ 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:
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
-- 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 : ℕ
_ : 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)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))

Tactic:
_
-- 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
rw : (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ (C * (u (k + 1) - u k)) • f (u (k + 1))
⊢ (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))

Tactic:
rw [smul_smul]

Premises used: smul_smul
-- 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
hb : 0 ≤ f (u (k + 1))
ha : u (k + 2) - u (k + 1) ≤ C * (u (k + 1) - u k)
⊢ (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ (C * (u (k + 1) - u k)) • f (u (k + 1))

Tactic:
gcongr
-- 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:
h_nonneg (u (k + 1))

Premises used: HAdd.hAdd, OfNat.ofNat