case base
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n : ℕ
⊢ f 0 - f 0 = 0

case step
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∑ i in range n, (f (i + 1) - f i) = f n - f 0
apply sum_range_induction
case step
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
case base
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n : ℕ
⊢ f 0 - f 0 = 0

case step
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
case base => apply tsub_self
no goals
case step
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
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₁]
no goals
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n : ℕ
⊢ f 0 - f 0 = 0
apply tsub_self
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n✝ n : ℕ
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n : ℕ
⊢ ∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
intro n
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
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)
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
f : ℕ → α
h : Monotone f
n✝ n : ℕ
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
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)
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
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)
have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
no goals
ι : Type ?u.627204
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝⁴ : CommMonoid β
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
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)
rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]