-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem sum_range_tsub [AddCommMonoid α] [PartialOrder α] [Sub α] [OrderedSub α]
    [AddLeftMono α] [AddLeftReflectLE α] [ExistsAddOfLE α]
    {f : ℕ → α} (h : Monotone f) (n : ℕ) :
    ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0

Proof state:
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0

Tactic:
apply sum_range_induction

Result:
case base
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ f 0 - f 0 = 0

case step
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Proof state:
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n✝ n : ℕ
h₁ : f n ≤ f (n + 1)
h₂ : f 0 ≤ f n
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]

Result:
no goals

Proof state:
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ f 0 - f 0 = 0

Tactic:
apply tsub_eq_of_eq_add

Result:
case h
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ f 0 = 0 + f 0

Proof state:
case step
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
case step =>
  intro n
  have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
  have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
  rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]

Result:
no goals

Proof state:
case h
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ f 0 = 0 + f 0

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
intro n

Result:
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n✝ n : ℕ
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Proof state:
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n✝ n : ℕ
h₁ : f n ≤ f (n + 1)
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
have h₂ : f 0 ≤ f n := h (Nat.zero_le _)

Result:
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n✝ n : ℕ
h₁ : f n ≤ f (n + 1)
h₂ : f 0 ≤ f n
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Proof state:
case base
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ f 0 - f 0 = 0

case step
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
case base => apply tsub_eq_of_eq_add; rw [zero_add]

Result:
case step
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Proof state:
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n✝ n : ℕ
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)

Result:
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : AddLeftMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : ExistsAddOfLE α
f : ℕ → α
h : Monotone f
n✝ n : ℕ
h₁ : f n ≤ f (n + 1)
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)