-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv :
  (↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
        ℕ → α)
      (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
        (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
          (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) =
    u n
h'v :
  Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)))
    (∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))),
      edist
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            (i + 1)))
        (f
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) m
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic m) ∧ ∀ i ∈ Iic m, u i ∈ s) v ⋯))) :
              ℕ → α)
            i)))
succ :
  ∃ (a : ℕ) (a_1 : ℕ → α),
    a_1 a = u (n + 1) ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
          ∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x))
⊢ ∃ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
    (↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
          (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) =
        u (n + 1) ∧
      Eq (α := ℝ≥0∞) (∑ x ∈ Finset.range (n + 1), edist (f (u (x + 1))) (f (u x)))
        (∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
          edist
            (f
              ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
                (i + 1)))
            (f
              ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
                i)))

Tactic:
simp only [Finset.sum_range_succ, Sigma.exists, Subtype.exists, mem_Iic, exists_and_left,
          exists_prop]

Premises used: Sigma.exists, Subtype.exists, exists_and_left, exists_prop, Set.mem_Iic, Finset.sum_range_succ