-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this_1 : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ≤ n then u i else v (i - (n + 1))
i :
  HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))
      (∑ i ∈ Finset.range m, edist (f (v (i + 1))) (f (v i))) =
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i)))
      (∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))))
i₁ :
  HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i)))
      (∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i)))) =
    HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i)))
      (∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i)))
i₂ :
  HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i)))
      (∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i))) ≤
    ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i))
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∑ i ∈ Finset.range (n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).1,
        edist (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) (i + 1)))
          (f ((↑(n, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ s) u ⋯).2 : ℕ → α) i)))
      (∑ i ∈ Finset.range (m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).1,
        edist (f ((↑(m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).2 : ℕ → α) (i + 1)))
          (f ((↑(m, Subtype.mk (p := fun (u : ℕ → α) ↦ Monotone u ∧ ∀ (i : ℕ), u i ∈ t) v ⋯).2 : ℕ → α) i))) ≤
    eVariationOn f (s ∪ t)

Tactic:
calc
    ((∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) +
          ∑ i ∈ Finset.range m, edist (f (v (i + 1))) (f (v i))) =
        (∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i))) +
          ∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))) := by
      dsimp only [w]
      congr 1
      · grind [Finset.sum_congr]
      · grind
    _ = (∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i))) +
          ∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i)) := by
      congr 1
      rw [Finset.range_eq_Ico]
      convert!
          Finset.sum_Ico_add (fun i : ℕ => edist (f (w (i + 1))) (f (w i))) 0 m (n + 1) using 3 <;>
        abel
    _ ≤ ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i)) := by
      rw [← Finset.sum_union]
      · gcongr; grind
      · exact Finset.disjoint_left.2 (by grind)
    _ ≤ eVariationOn f (s ∪ t) := sum_le (by grind [Monotone]) (by grind)

Premises used: Finset.Ico, eVariationOn, Finset.range, eVariationOn.sum_le, HAdd.hAdd, EDist.edist, Union.union, OfNat.ofNat, Finset.sum