-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem MonotoneOn.eVariationOn_le {f : α → ℝ} {s : Set α} (hf : MonotoneOn f s) {a b : α}
    (as : a ∈ s) (bs : b ∈ s) : eVariationOn f (s ∩ Icc a b) ≤ ENNReal.ofReal (f b - f a)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
a✝ : i ∈ Finset.range n
⊢ 0 ≤ f (u (i + 1)) - f (u i)

Tactic:
exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) = ENNReal.ofReal (f (u n) - f (u 0))

Tactic:
rw [Finset.sum_range_sub fun i => f (u i)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) = ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i))

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Result:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i ∈ Finset.range n
⊢ edist (f (u (i + 1))) (f (u i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ENNReal.ofReal (f (u n) - f (u 0)) ≤ ENNReal.ofReal (f b - f a)

Tactic:
apply ENNReal.ofReal_le_ofReal

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ f (u n) - f (u 0) ≤ f b - f a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ∀ i ∈ Finset.range n, 0 ≤ f (u (i + 1)) - f (u i)

Tactic:
intro i _

Result:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
a✝ : i ∈ Finset.range n
⊢ 0 ≤ f (u (i + 1)) - f (u i)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i < n
⊢ edist (f (u (i + 1))) (f (u i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))

Tactic:
rw [edist_dist, Real.dist_eq, abs_of_nonneg]

Result:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i < n
⊢ 0 ≤ f (u (i + 1)) - f (u i)

Proof state:
case mk.mk.intro
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) ≤
    ENNReal.ofReal (f b - f a)

Tactic:
calc
  (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
      ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) := by
    refine Finset.sum_congr rfl fun i hi => ?_
    simp only [Finset.mem_range] at hi
    rw [edist_dist, Real.dist_eq, abs_of_nonneg]
    exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
  _ = ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i))) := by
    rw [ENNReal.ofReal_sum_of_nonneg]
    intro i _
    exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
  _ = ENNReal.ofReal (f (u n) - f (u 0)) := by rw [Finset.sum_range_sub fun i => f (u i)]
  _ ≤ ENNReal.ofReal (f b - f a) := by
    apply ENNReal.ofReal_le_ofReal
    exact sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
⊢ eVariationOn f (s ∩ Icc a b) ≤ ENNReal.ofReal (f b - f a)

Tactic:
apply iSup_le _

Result:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b }),
    ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) ≤ ENNReal.ofReal (f b - f a)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∩ Icc a b }),
    ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) ≤ ENNReal.ofReal (f b - f a)

Tactic:
rintro ⟨n, ⟨u, hu, us⟩⟩

Result:
case mk.mk.intro
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) ≤
    ENNReal.ofReal (f b - f a)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i ∈ Finset.range n
⊢ edist (f (u (i + 1))) (f (u i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))

Tactic:
simp only [Finset.mem_range] at hi

Result:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i < n
⊢ edist (f (u (i + 1))) (f (u i)) = ENNReal.ofReal (f (u (i + 1)) - f (u i))

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
i : ℕ
hi : i < n
⊢ 0 ≤ f (u (i + 1)) - f (u i)

Tactic:
exact sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ f (u n) - f (u 0) ≤ f b - f a

Tactic:
exact sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ∑ i ∈ Finset.range n, ENNReal.ofReal (f (u (i + 1)) - f (u i)) =
    ENNReal.ofReal (∑ i ∈ Finset.range n, (f (u (i + 1)) - f (u i)))

Tactic:
rw [ENNReal.ofReal_sum_of_nonneg]

Result:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : MonotoneOn f s
a b : α
as : a ∈ s
bs : b ∈ s
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s ∩ Icc a b
⊢ ∀ i ∈ Finset.range n, 0 ≤ f (u (i + 1)) - f (u i)