Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : 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 : ∑ 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)) ≤
    ∑ i ∈ Ico (u 0 + 1) ?n, f i + ∑ i ∈ Ico ?n (u (n + 1) + 1), f i

pp: case n
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : 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 : ∑ 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
⊢ ℕ

pp: case hmn
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : 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 : ∑ 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 ≤ ?n

pp: case hnk
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : 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 : ∑ 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
⊢ ?n ≤ u (n + 1) + 1

Tactic:
]

Goal state after:
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : 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 : ∑ 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)) ≤
    ∑ i ∈ Ico (u 0 + 1) ?n, f i + ∑ i ∈ Ico ?n (u (n + 1) + 1), f i

case n
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : 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 : ∑ 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
⊢ ℕ

case hmn
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : 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 : ∑ 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 ≤ ?n

case hnk
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : 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 : ∑ 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
⊢ ?n ≤ u (n + 1) + 1