-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem sum_le_of_monotoneOn_Icc (f : α → E) {s : Set α} {m n : ℕ} {u : ℕ → α}
    (hu : MonotoneOn u (Icc m n)) (us : ∀ i ∈ Icc m n, u i ∈ s) :
    (∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i))) ≤ eVariationOn f s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : ℕ → ↑(Icc m n) := projIcc m n hmn
v : ℕ → α := fun i => u ↑(π i)
i : ℕ
hi : m ≤ i ∧ i < n
⊢ edist (f (u (i + 1))) (f (u i)) = edist (f (v (i + 1))) (f (v i))

Tactic:
simp only [v, π, projIcc_of_mem hmn ⟨hi.1, hi.2.le⟩,
  projIcc_of_mem hmn ⟨hi.1.trans i.le_succ, hi.2⟩]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : ℕ → ↑(Icc m n) := projIcc m n hmn
v : ℕ → α := fun i => u ↑(π i)
i : ℕ
hi : i ∈ Finset.Ico m n
⊢ edist (f (u (i + 1))) (f (u i)) = edist (f (v (i + 1))) (f (v i))

Tactic:
rw [Finset.mem_Ico] at hi

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : ℕ → ↑(Icc m n) := projIcc m n hmn
v : ℕ → α := fun i => u ↑(π i)
i : ℕ
hi : m ≤ i ∧ i < n
⊢ edist (f (u (i + 1))) (f (u i)) = edist (f (v (i + 1))) (f (v i))

Proof state:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : ℕ → ↑(Icc m n) := projIcc m n hmn
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
let v i := u (π i)

Result:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : ℕ → ↑(Icc m n) := projIcc m n hmn
v : ℕ → α := fun i => u ↑(π i)
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
rcases le_total n m with hnm | hmn

Result:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hnm : n ≤ m
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Proof state:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : ℕ → ↑(Icc m n) := projIcc m n hmn
v : ℕ → α := fun i => u ↑(π i)
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
calc
  ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i))
      = ∑ i ∈ Finset.Ico m n, edist (f (v (i + 1))) (f (v i)) :=
    Finset.sum_congr rfl fun i hi ↦ by
      rw [Finset.mem_Ico] at hi
      simp only [v, π, projIcc_of_mem hmn ⟨hi.1, hi.2.le⟩,
        projIcc_of_mem hmn ⟨hi.1.trans i.le_succ, hi.2⟩]
  _ ≤ ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) :=
    Finset.sum_mono_set _ (Nat.Iio_eq_range ▸ Finset.Ico_subset_Iio_self)
  _ ≤ eVariationOn f s :=
    sum_le _ _ (fun i j h ↦ hu (π i).2 (π j).2 (monotone_projIcc hmn h)) fun i ↦ us _ (π i).2

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
let π := projIcc m n hmn

Result:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : ℕ → ↑(Icc m n) := projIcc m n hmn
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Proof state:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hnm : n ≤ m
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
simp [Finset.Ico_eq_empty_of_le hnm]

Result:
no goals