From 01c6643dcd0f0162133a61f117dd8ffd76055e59 Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Wed, 8 Jul 2026 17:15:33 -0700
Subject: [PATCH 01/26] Bounded variation lemmas

---
 .../EMetricSpace/BoundedVariation.lean        | 86 +++++++++++++++++++
 1 file changed, 86 insertions(+)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 20e89be5466d28..cf22ff476a03d2 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Order.Interval.Set.ProjIcc
+public import Mathlib.Data.Finset.Sort
 public import Mathlib.Tactic.Finiteness
 public import Mathlib.Topology.UniformSpace.UniformConvergenceTopology
 public import Mathlib.Topology.Instances.ENNReal.Lemmas
@@ -219,6 +220,10 @@ protected theorem subsingleton (f : α → E) {s : Set α} (hs : s.Subsingleton)
     eVariationOn f s = 0 :=
   constant_on (hs.image f)
 
+@[simp]
+lemma _root_.BoundedVariationOn.ofSubsingleton {f : α → E} {s : Set α} (h : s.Subsingleton) :
+    BoundedVariationOn f s := by simp [BoundedVariationOn, h]
+
 theorem lowerSemicontinuous_aux {ι : Type*} {F : ι → α → E} {p : Filter ι} {f : α → E} {s : Set α}
     (Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))) {v : ℝ≥0∞} (hv : v < eVariationOn f s) :
     ∀ᶠ n : ι in p, v < eVariationOn (F n) s := by
@@ -427,6 +432,67 @@ theorem sum' (f : α → E) {I : ℕ → α} (hI : Monotone I) {n : ℕ} :
     gcongr <;> (apply hI; rw [Finset.mem_range] at hi; lia)
   · simp
 
+@[simp]
+theorem pair (f : α → E) (a b : α) : eVariationOn f {a, b} = edist (f a) (f b) := by
+  wlog hab : a ≤ b generalizing a b
+  · simpa [edist_comm, pair_comm] using this b a (le_of_not_ge hab)
+  · apply le_antisymm _ (edist_le f (by simp) (by simp))
+    simp only [eVariationOn_eq_strictMonoOn, iSup_le_iff]
+    rintro ⟨ n, ⟨ u, ⟨ hmono, hi ⟩ ⟩ ⟩
+    rcases (by omega : n = 0 ∨ n = 1 ∨ 2 ≤ n) with rfl | rfl | hn
+    · simp
+    · have : u 0 < u 1 := hmono (by simp) (by simp) (by norm_num)
+      simp [(by grind : u 0 = a), (by grind : u 1 = b), edist_comm]
+    have : u 0 < u 1 := hmono (by simp) (by grind) (by norm_num)
+    have : u 1 < u 2 := hmono (by grind) (by grind) (by norm_num)
+    grind
+
+/-- A generalization of `eVariationOn.union` in which the greatest element of `s` is allowed to lie
+to the left of the least element of `t`. -/
+theorem union' (f : α → E) {s t : Set α} {x y : α} (hs : IsGreatest s x) (ht : IsLeast t y)
+    (hxy : x ≤ y) :
+    eVariationOn f (s ∪ t) = eVariationOn f s + edist (f x) (f y) + eVariationOn f t := calc
+  _ = eVariationOn f ((s ∪ {x, y}) ∪ t) := by congr 1; grind [hs.1, ht.1]
+  _ = eVariationOn f (s ∪ {x, y}) + eVariationOn f t := by
+    apply union f _ ht
+    simp [IsGreatest, hxy, upperBounds_mono_mem hxy hs.2]
+  _ = eVariationOn f s + eVariationOn f {x, y} + eVariationOn f t := by
+    congr
+    apply union f hs _
+    simp [IsLeast, hxy]
+  _ = _ := by simp [pair]
+
+theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u) (n : ℕ) :
+    eVariationOn f (u '' .Iic n) = ∑ i ∈ .range n, edist (f (u i)) (f (u (i + 1))) := by
+  induction n with
+  | zero => simp [(by grind : Iic 0 = {0})]
+  | succ n ih => calc
+    _ = eVariationOn f (u '' .Iic n ∪ {u n, u (n + 1)}) := by congr; grind
+    _ = eVariationOn f (u '' .Iic n) + eVariationOn f {u n, u (n + 1)} := by
+      apply union f (x := u n) _ _
+      · simp only [IsGreatest, mem_image, mem_Iic, mem_upperBounds, forall_exists_index, and_imp,
+        forall_apply_eq_imp_iff₂]
+        refine ⟨ ⟨ n, by simp ⟩, fun a ha ↦ hu ha ⟩
+      · simp [IsLeast, hu (by omega : n ≤ n + 1)]
+    _ = _ := by
+      simp [Finset.sum_range_succ, ih]
+
+@[simp]
+theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α → E) (s : Finset α)
+    : BoundedVariationOn f s := by
+  let k := s.card
+  by_cases h : k = 0
+  · simp [k] at h; simp [h]
+  let u : ℕ → α := fun n ↦ s.orderEmbOfFin (by rfl : _ = k) ⟨ min n (k - 1), by grind ⟩
+  have : s = u '' .Iic (k - 1) := by
+    rw [← s.range_orderEmbOfFin (by rfl : _ = k)]
+    ext x; simp only [mem_image, mem_Iic, mem_range, u]
+    constructor
+    · rintro ⟨ i, rfl ⟩; exact ⟨ i.val, by grind ⟩
+    · rintro ⟨ i, hi, rfl ⟩; use ⟨ i, by omega ⟩; congr; omega
+  have hmono : Monotone u := fun _ _ _ ↦ OrderEmbedding.monotone _ (by grind)
+  simp [BoundedVariationOn, this, image_range_of_monotone f hmono _]
+
 /-! ### Composition of bounded variation functions with monotone functions -/
 
 section Monotone
@@ -1128,6 +1194,26 @@ theorem MonotoneOn.boundedVariationOn
   grw [hf.eVariationOn_le as bs]
   exact ENNReal.ofReal_mono (by grind)
 
+theorem MonotoneOn.eVariationOn_eq {f : α → ℝ} {s : Set α}
+    (hf : MonotoneOn f s) {a b : α} (hab : a ≤ b) (as : a ∈ s) (bs : b ∈ s) :
+    eVariationOn f (s ∩ .Icc a b) = ENNReal.ofReal (f b - f a) := by
+  have h : BoundedVariationOn f (s ∩ .Icc a b) := hf.locallyBoundedVariationOn a b as bs
+  apply eq_of_le_of_ge (eVariationOn_le hf as bs) (ENNReal.ofReal_le_of_le_toReal _)
+  grw [← BoundedVariationOn.dist_le h (x := a) (y := b)] <;> grind [Real.dist_eq]
+
+lemma eVariationOn_id {a b : ℝ} (hab : a ≤ b) {s : Set ℝ} (as : a ∈ s) (bs : b ∈ s) :
+    eVariationOn id (s ∩ .Icc a b) = ENNReal.ofReal (b - a) :=
+  MonotoneOn.eVariationOn_eq (monotone_id.monotoneOn _) hab as bs
+
+@[simp]
+lemma eVariationOn_id_Icc {a b : ℝ} (hab : a ≤ b) :
+  eVariationOn id (.Icc a b) = ENNReal.ofReal (b - a) := by
+  simpa using eVariationOn_id hab (s := Set.univ) (by simp) (by simp)
+
+@[simp]
+lemma BoundedVariationOn.id_of_Icc {a b : ℝ} :  BoundedVariationOn id (.Icc a b) := by
+  rcases lt_or_ge b a with hab | hab <;> simp [hab, BoundedVariationOn, eVariationOn_id_Icc]
+
 /-! ### Lipschitz functions and bounded variation -/
 
 section LipschitzOnWith

From fefc307b4a7cc8c8ded518e71b1d5b656a8f487b Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Wed, 8 Jul 2026 18:09:37 -0700
Subject: [PATCH 02/26] polish

---
 .../EMetricSpace/BoundedVariation.lean        | 44 ++++++++++++-------
 1 file changed, 28 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index cf22ff476a03d2..c953839b5621bb 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -220,8 +220,9 @@ protected theorem subsingleton (f : α → E) {s : Set α} (hs : s.Subsingleton)
     eVariationOn f s = 0 :=
   constant_on (hs.image f)
 
+/-- A function has bounded variation on any subsingleton set. -/
 @[simp]
-lemma _root_.BoundedVariationOn.ofSubsingleton {f : α → E} {s : Set α} (h : s.Subsingleton) :
+lemma _root_.BoundedVariationOn.of_subsingleton {f : α → E} {s : Set α} (h : s.Subsingleton) :
     BoundedVariationOn f s := by simp [BoundedVariationOn, h]
 
 theorem lowerSemicontinuous_aux {ι : Type*} {F : ι → α → E} {p : Filter ι} {f : α → E} {s : Set α}
@@ -432,19 +433,20 @@ theorem sum' (f : α → E) {I : ℕ → α} (hI : Monotone I) {n : ℕ} :
     gcongr <;> (apply hI; rw [Finset.mem_range] at hi; lia)
   · simp
 
+/-- The variation of `f` on a two-point set `{a, b}` is the distance between its two values. -/
 @[simp]
 theorem pair (f : α → E) (a b : α) : eVariationOn f {a, b} = edist (f a) (f b) := by
   wlog hab : a ≤ b generalizing a b
   · simpa [edist_comm, pair_comm] using this b a (le_of_not_ge hab)
   · apply le_antisymm _ (edist_le f (by simp) (by simp))
     simp only [eVariationOn_eq_strictMonoOn, iSup_le_iff]
-    rintro ⟨ n, ⟨ u, ⟨ hmono, hi ⟩ ⟩ ⟩
+    rintro ⟨n, u, hmono, hi⟩
     rcases (by omega : n = 0 ∨ n = 1 ∨ 2 ≤ n) with rfl | rfl | hn
     · simp
-    · have : u 0 < u 1 := hmono (by simp) (by simp) (by norm_num)
+    · have : u 0 < u 1 := hmono (by simp) (by simp) zero_lt_one
       simp [(by grind : u 0 = a), (by grind : u 1 = b), edist_comm]
-    have : u 0 < u 1 := hmono (by simp) (by grind) (by norm_num)
-    have : u 1 < u 2 := hmono (by grind) (by grind) (by norm_num)
+    have : u 0 < u 1 := hmono (by simp) (by grind) zero_lt_one
+    have : u 1 < u 2 := hmono (by grind) (by grind) one_lt_two
     grind
 
 /-- A generalization of `eVariationOn.union` in which the greatest element of `s` is allowed to lie
@@ -462,34 +464,39 @@ theorem union' (f : α → E) {s t : Set α} {x y : α} (hs : IsGreatest s x) (h
     simp [IsLeast, hxy]
   _ = _ := by simp [pair]
 
+/-- The variation of `f` along the image of `{0, …, n}` under a monotone sequence `u` is the sum of
+the distances between consecutive values. -/
 theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u) (n : ℕ) :
     eVariationOn f (u '' .Iic n) = ∑ i ∈ .range n, edist (f (u i)) (f (u (i + 1))) := by
   induction n with
-  | zero => simp [(by grind : Iic 0 = {0})]
+  | zero => simp [(by aesop : Iic 0 = {0})]
   | succ n ih => calc
     _ = eVariationOn f (u '' .Iic n ∪ {u n, u (n + 1)}) := by congr; grind
     _ = eVariationOn f (u '' .Iic n) + eVariationOn f {u n, u (n + 1)} := by
       apply union f (x := u n) _ _
       · simp only [IsGreatest, mem_image, mem_Iic, mem_upperBounds, forall_exists_index, and_imp,
         forall_apply_eq_imp_iff₂]
-        refine ⟨ ⟨ n, by simp ⟩, fun a ha ↦ hu ha ⟩
+        refine ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
       · simp [IsLeast, hu (by omega : n ≤ n + 1)]
     _ = _ := by
       simp [Finset.sum_range_succ, ih]
 
+/-- A function valued in a metric space has bounded variation on any finite set (the finiteness of
+the space's distances makes the total variation finite). -/
 @[simp]
-theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α → E) (s : Finset α)
-    : BoundedVariationOn f s := by
+theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α → E) (s : Finset α) :
+    BoundedVariationOn f s := by
+  obtain rfl | hne := s.eq_empty_or_nonempty
+  · simp
   let k := s.card
-  by_cases h : k = 0
-  · simp [k] at h; simp [h]
-  let u : ℕ → α := fun n ↦ s.orderEmbOfFin (by rfl : _ = k) ⟨ min n (k - 1), by grind ⟩
+  have hk : 0 < k := s.card_pos.2 hne
+  let u : ℕ → α := fun n ↦ s.orderEmbOfFin (by rfl : _ = k) ⟨min n (k - 1), by grind⟩
   have : s = u '' .Iic (k - 1) := by
     rw [← s.range_orderEmbOfFin (by rfl : _ = k)]
     ext x; simp only [mem_image, mem_Iic, mem_range, u]
     constructor
-    · rintro ⟨ i, rfl ⟩; exact ⟨ i.val, by grind ⟩
-    · rintro ⟨ i, hi, rfl ⟩; use ⟨ i, by omega ⟩; congr; omega
+    · rintro ⟨i, rfl⟩; exact ⟨i.val, by grind⟩
+    · rintro ⟨i, hi, rfl⟩; use ⟨i, by omega⟩; congr; omega
   have hmono : Monotone u := fun _ _ _ ↦ OrderEmbedding.monotone _ (by grind)
   simp [BoundedVariationOn, this, image_range_of_monotone f hmono _]
 
@@ -1194,6 +1201,8 @@ theorem MonotoneOn.boundedVariationOn
   grw [hf.eVariationOn_le as bs]
   exact ENNReal.ofReal_mono (by grind)
 
+/-- The variation of a monotone real-valued function on `s ∩ Icc a b` equals its increment
+`f b - f a`. -/
 theorem MonotoneOn.eVariationOn_eq {f : α → ℝ} {s : Set α}
     (hf : MonotoneOn f s) {a b : α} (hab : a ≤ b) (as : a ∈ s) (bs : b ∈ s) :
     eVariationOn f (s ∩ .Icc a b) = ENNReal.ofReal (f b - f a) := by
@@ -1201,17 +1210,20 @@ theorem MonotoneOn.eVariationOn_eq {f : α → ℝ} {s : Set α}
   apply eq_of_le_of_ge (eVariationOn_le hf as bs) (ENNReal.ofReal_le_of_le_toReal _)
   grw [← BoundedVariationOn.dist_le h (x := a) (y := b)] <;> grind [Real.dist_eq]
 
+/-- The variation of the identity on `s ∩ Icc a b` is `b - a`. -/
 lemma eVariationOn_id {a b : ℝ} (hab : a ≤ b) {s : Set ℝ} (as : a ∈ s) (bs : b ∈ s) :
     eVariationOn id (s ∩ .Icc a b) = ENNReal.ofReal (b - a) :=
   MonotoneOn.eVariationOn_eq (monotone_id.monotoneOn _) hab as bs
 
+/-- The variation of the identity on `Icc a b` is `b - a`. -/
 @[simp]
 lemma eVariationOn_id_Icc {a b : ℝ} (hab : a ≤ b) :
-  eVariationOn id (.Icc a b) = ENNReal.ofReal (b - a) := by
+    eVariationOn id (.Icc a b) = ENNReal.ofReal (b - a) := by
   simpa using eVariationOn_id hab (s := Set.univ) (by simp) (by simp)
 
+/-- The identity function has bounded variation on every interval `Icc a b`. -/
 @[simp]
-lemma BoundedVariationOn.id_of_Icc {a b : ℝ} :  BoundedVariationOn id (.Icc a b) := by
+lemma BoundedVariationOn.id_Icc {a b : ℝ} : BoundedVariationOn id (.Icc a b) := by
   rcases lt_or_ge b a with hab | hab <;> simp [hab, BoundedVariationOn, eVariationOn_id_Icc]
 
 /-! ### Lipschitz functions and bounded variation -/

From fef9cfcc0f2de1e299e3d065f2387a4ccb32246a Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 08:02:45 -0700
Subject: [PATCH 03/26] strengthen simp lemma for bounded variation on finite

---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index c953839b5621bb..d0b4c6ebb0cc41 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -221,7 +221,6 @@ protected theorem subsingleton (f : α → E) {s : Set α} (hs : s.Subsingleton)
   constant_on (hs.image f)
 
 /-- A function has bounded variation on any subsingleton set. -/
-@[simp]
 lemma _root_.BoundedVariationOn.of_subsingleton {f : α → E} {s : Set α} (h : s.Subsingleton) :
     BoundedVariationOn f s := by simp [BoundedVariationOn, h]
 
@@ -481,13 +480,12 @@ theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u
     _ = _ := by
       simp [Finset.sum_range_succ, ih]
 
-/-- A function valued in a metric space has bounded variation on any finite set (the finiteness of
+/-- A function valued in a metric space has bounded variation on any `Finset` (the finiteness of
 the space's distances makes the total variation finite). -/
-@[simp]
 theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α → E) (s : Finset α) :
     BoundedVariationOn f s := by
   obtain rfl | hne := s.eq_empty_or_nonempty
-  · simp
+  · simp [BoundedVariationOn.of_subsingleton]
   let k := s.card
   have hk : 0 < k := s.card_pos.2 hne
   let u : ℕ → α := fun n ↦ s.orderEmbOfFin (by rfl : _ = k) ⟨min n (k - 1), by grind⟩
@@ -500,6 +498,12 @@ theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α 
   have hmono : Monotone u := fun _ _ _ ↦ OrderEmbedding.monotone _ (by grind)
   simp [BoundedVariationOn, this, image_range_of_monotone f hmono _]
 
+/-- A version of the previous theorem for `Finite` sets. -/
+@[simp]
+theorem _root_.BoundedVariationOn.of_finite {E} [PseudoMetricSpace E] (f : α → E) (s : Set α)
+[Finite s] : BoundedVariationOn f s := by
+  simpa using BoundedVariationOn.of_finset f s.toFinite.toFinset
+
 /-! ### Composition of bounded variation functions with monotone functions -/
 
 section Monotone

From 47e479de8ea414ff9997654667e72c457a2c2706 Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:10:31 -0700
Subject: [PATCH 04/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index d0b4c6ebb0cc41..bf8d889f7b18cd 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -444,9 +444,9 @@ theorem pair (f : α → E) (a b : α) : eVariationOn f {a, b} = edist (f a) (f
     · simp
     · have : u 0 < u 1 := hmono (by simp) (by simp) zero_lt_one
       simp [(by grind : u 0 = a), (by grind : u 1 = b), edist_comm]
-    have : u 0 < u 1 := hmono (by simp) (by grind) zero_lt_one
-    have : u 1 < u 2 := hmono (by grind) (by grind) one_lt_two
-    grind
+    · have : u 0 < u 1 := hmono (by simp) (by grind) zero_lt_one
+      have : u 1 < u 2 := hmono (by grind) (by grind) one_lt_two
+      grind
 
 /-- A generalization of `eVariationOn.union` in which the greatest element of `s` is allowed to lie
 to the left of the least element of `t`. -/

From a7facd4968518ec49e0fd20e29e2e87ede74f05a Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:10:46 -0700
Subject: [PATCH 05/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index bf8d889f7b18cd..b12d470ef7f9e1 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -476,7 +476,7 @@ theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u
       · simp only [IsGreatest, mem_image, mem_Iic, mem_upperBounds, forall_exists_index, and_imp,
         forall_apply_eq_imp_iff₂]
         refine ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
-      · simp [IsLeast, hu (by omega : n ≤ n + 1)]
+      · simp [IsLeast, hu n.le_succ]
     _ = _ := by
       simp [Finset.sum_range_succ, ih]
 

From 7e6b4f6295d84bb2e21a7b15d6fc5d107a15a5ce Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:11:02 -0700
Subject: [PATCH 06/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index b12d470ef7f9e1..0dd4ecfd7742ac 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -490,8 +490,8 @@ theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α 
   have hk : 0 < k := s.card_pos.2 hne
   let u : ℕ → α := fun n ↦ s.orderEmbOfFin (by rfl : _ = k) ⟨min n (k - 1), by grind⟩
   have : s = u '' .Iic (k - 1) := by
-    rw [← s.range_orderEmbOfFin (by rfl : _ = k)]
-    ext x; simp only [mem_image, mem_Iic, mem_range, u]
+    ext
+    simp only [← s.range_orderEmbOfFin rfl, mem_image, mem_Iic, mem_range, u]
     constructor
     · rintro ⟨i, rfl⟩; exact ⟨i.val, by grind⟩
     · rintro ⟨i, hi, rfl⟩; use ⟨i, by omega⟩; congr; omega

From 04f6150c877871a718df406cc74ad16ff33627e4 Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:11:19 -0700
Subject: [PATCH 07/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 0dd4ecfd7742ac..99c30f979d44d5 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -1217,7 +1217,7 @@ theorem MonotoneOn.eVariationOn_eq {f : α → ℝ} {s : Set α}
 /-- The variation of the identity on `s ∩ Icc a b` is `b - a`. -/
 lemma eVariationOn_id {a b : ℝ} (hab : a ≤ b) {s : Set ℝ} (as : a ∈ s) (bs : b ∈ s) :
     eVariationOn id (s ∩ .Icc a b) = ENNReal.ofReal (b - a) :=
-  MonotoneOn.eVariationOn_eq (monotone_id.monotoneOn _) hab as bs
+  (monotone_id.monotoneOn _).eVariationOn_eq hab as bs
 
 /-- The variation of the identity on `Icc a b` is `b - a`. -/
 @[simp]

From 77cf417816c8a04c0083bd962eb79f0298c783ef Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:12:02 -0700
Subject: [PATCH 08/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 99c30f979d44d5..142445f3f50066 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -1223,7 +1223,7 @@ lemma eVariationOn_id {a b : ℝ} (hab : a ≤ b) {s : Set ℝ} (as : a ∈ s) (
 @[simp]
 lemma eVariationOn_id_Icc {a b : ℝ} (hab : a ≤ b) :
     eVariationOn id (.Icc a b) = ENNReal.ofReal (b - a) := by
-  simpa using eVariationOn_id hab (s := Set.univ) (by simp) (by simp)
+  simpa using eVariationOn_id hab (s := univ) (by simp) (by simp)
 
 /-- The identity function has bounded variation on every interval `Icc a b`. -/
 @[simp]

From 46d147f1274ecd66501c62e3b3eefe46fb9e84fd Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:12:18 -0700
Subject: [PATCH 09/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 142445f3f50066..3d0c3b70607ce2 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -1212,7 +1212,7 @@ theorem MonotoneOn.eVariationOn_eq {f : α → ℝ} {s : Set α}
     eVariationOn f (s ∩ .Icc a b) = ENNReal.ofReal (f b - f a) := by
   have h : BoundedVariationOn f (s ∩ .Icc a b) := hf.locallyBoundedVariationOn a b as bs
   apply eq_of_le_of_ge (eVariationOn_le hf as bs) (ENNReal.ofReal_le_of_le_toReal _)
-  grw [← BoundedVariationOn.dist_le h (x := a) (y := b)] <;> grind [Real.dist_eq]
+  grw [← h.dist_le (x := a) (y := b)] <;> grind [Real.dist_eq]
 
 /-- The variation of the identity on `s ∩ Icc a b` is `b - a`. -/
 lemma eVariationOn_id {a b : ℝ} (hab : a ≤ b) {s : Set ℝ} (as : a ∈ s) (bs : b ∈ s) :

From 6197e070c1ef16a725181f72532131f0175c99a6 Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:12:29 -0700
Subject: [PATCH 10/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 3d0c3b70607ce2..58936916e1c396 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -477,8 +477,7 @@ theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u
         forall_apply_eq_imp_iff₂]
         refine ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
       · simp [IsLeast, hu n.le_succ]
-    _ = _ := by
-      simp [Finset.sum_range_succ, ih]
+    _ = _ := by simp [Finset.sum_range_succ, ih]
 
 /-- A function valued in a metric space has bounded variation on any `Finset` (the finiteness of
 the space's distances makes the total variation finite). -/

From cba47d2690b81f927f15d3ada40d3fe7a7b5a86d Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:12:37 -0700
Subject: [PATCH 11/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 58936916e1c396..dd3be223008ebe 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -468,7 +468,7 @@ the distances between consecutive values. -/
 theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u) (n : ℕ) :
     eVariationOn f (u '' .Iic n) = ∑ i ∈ .range n, edist (f (u i)) (f (u (i + 1))) := by
   induction n with
-  | zero => simp [(by aesop : Iic 0 = {0})]
+  | zero => simp [Iic]
   | succ n ih => calc
     _ = eVariationOn f (u '' .Iic n ∪ {u n, u (n + 1)}) := by congr; grind
     _ = eVariationOn f (u '' .Iic n) + eVariationOn f {u n, u (n + 1)} := by

From 8e08c704530a1b75de2e311c506dbe5ac99df5a8 Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:12:57 -0700
Subject: [PATCH 12/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index dd3be223008ebe..6ff86ed94613f1 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -466,7 +466,7 @@ theorem union' (f : α → E) {s t : Set α} {x y : α} (hs : IsGreatest s x) (h
 /-- The variation of `f` along the image of `{0, …, n}` under a monotone sequence `u` is the sum of
 the distances between consecutive values. -/
 theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u) (n : ℕ) :
-    eVariationOn f (u '' .Iic n) = ∑ i ∈ .range n, edist (f (u i)) (f (u (i + 1))) := by
+    eVariationOn f (u '' Iic n) = ∑ i ∈ .range n, edist (f (u i)) (f (u (i + 1))) := by
   induction n with
   | zero => simp [Iic]
   | succ n ih => calc

From b3e0eedd68b7dde118260efb1454658e7a2d49d0 Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:13:32 -0700
Subject: [PATCH 13/26] whitespace

---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index d0b4c6ebb0cc41..48309c841ff168 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -505,7 +505,6 @@ theorem _root_.BoundedVariationOn.of_finite {E} [PseudoMetricSpace E] (f : α 
   simpa using BoundedVariationOn.of_finset f s.toFinite.toFinset
 
 /-! ### Composition of bounded variation functions with monotone functions -/
-
 section Monotone
 
 variable {β : Type*} [LinearOrder β]

From 9217ed395f65e76d15eb4b128b03a0fc6a940cb9 Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:25:46 -0700
Subject: [PATCH 14/26] golf dot notation

---
 .../EMetricSpace/BoundedVariation.lean        | 34 ++++++++++---------
 1 file changed, 18 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 31db8925e78a09..e42c44e733e0a2 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -470,8 +470,8 @@ theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u
   induction n with
   | zero => simp [Iic]
   | succ n ih => calc
-    _ = eVariationOn f (u '' .Iic n ∪ {u n, u (n + 1)}) := by congr; grind
-    _ = eVariationOn f (u '' .Iic n) + eVariationOn f {u n, u (n + 1)} := by
+    _ = eVariationOn f (u '' Iic n ∪ {u n, u (n + 1)}) := by congr; grind
+    _ = eVariationOn f (u '' Iic n) + eVariationOn f {u n, u (n + 1)} := by
       apply union f (x := u n) _ _
       · simp only [IsGreatest, mem_image, mem_Iic, mem_upperBounds, forall_exists_index, and_imp,
         forall_apply_eq_imp_iff₂]
@@ -488,9 +488,9 @@ theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α 
   let k := s.card
   have hk : 0 < k := s.card_pos.2 hne
   let u : ℕ → α := fun n ↦ s.orderEmbOfFin (by rfl : _ = k) ⟨min n (k - 1), by grind⟩
-  have : s = u '' .Iic (k - 1) := by
+  have : s = u '' Iic (k - 1) := by
     ext
-    simp only [← s.range_orderEmbOfFin rfl, mem_image, mem_Iic, mem_range, u]
+    simp only [← s.range_orderEmbOfFin (rfl : _ = k), mem_image, mem_Iic, mem_range, u]
     constructor
     · rintro ⟨i, rfl⟩; exact ⟨i.val, by grind⟩
     · rintro ⟨i, hi, rfl⟩; use ⟨i, by omega⟩; congr; omega
@@ -1206,26 +1206,28 @@ theorem MonotoneOn.boundedVariationOn
 /-- The variation of a monotone real-valued function on `s ∩ Icc a b` equals its increment
 `f b - f a`. -/
 theorem MonotoneOn.eVariationOn_eq {f : α → ℝ} {s : Set α}
-    (hf : MonotoneOn f s) {a b : α} (hab : a ≤ b) (as : a ∈ s) (bs : b ∈ s) :
-    eVariationOn f (s ∩ .Icc a b) = ENNReal.ofReal (f b - f a) := by
-  have h : BoundedVariationOn f (s ∩ .Icc a b) := hf.locallyBoundedVariationOn a b as bs
-  apply eq_of_le_of_ge (eVariationOn_le hf as bs) (ENNReal.ofReal_le_of_le_toReal _)
-  grw [← h.dist_le (x := a) (y := b)] <;> grind [Real.dist_eq]
+    (hf : MonotoneOn f s) {a b : α} (as : a ∈ s) (bs : b ∈ s) :
+    eVariationOn f (s ∩ Icc a b) = ENNReal.ofReal (f b - f a) := by
+  rcases le_or_gt a b with hab | hab
+  · have h : BoundedVariationOn f (s ∩ Icc a b) := hf.locallyBoundedVariationOn a b as bs
+    apply eq_of_le_of_ge (eVariationOn_le hf as bs) (ENNReal.ofReal_le_of_le_toReal _)
+    grw [← h.dist_le (x := a) (y := b)] <;> grind [Real.dist_eq]
+  · simp [hab, hf bs as hab.le]
 
 /-- The variation of the identity on `s ∩ Icc a b` is `b - a`. -/
-lemma eVariationOn_id {a b : ℝ} (hab : a ≤ b) {s : Set ℝ} (as : a ∈ s) (bs : b ∈ s) :
-    eVariationOn id (s ∩ .Icc a b) = ENNReal.ofReal (b - a) :=
-  (monotone_id.monotoneOn _).eVariationOn_eq hab as bs
+lemma eVariationOn_id {a b : ℝ} {s : Set ℝ} (as : a ∈ s) (bs : b ∈ s) :
+    eVariationOn id (s ∩ Icc a b) = ENNReal.ofReal (b - a) :=
+  (monotone_id.monotoneOn _).eVariationOn_eq as bs
 
 /-- The variation of the identity on `Icc a b` is `b - a`. -/
 @[simp]
-lemma eVariationOn_id_Icc {a b : ℝ} (hab : a ≤ b) :
-    eVariationOn id (.Icc a b) = ENNReal.ofReal (b - a) := by
-  simpa using eVariationOn_id hab (s := univ) (by simp) (by simp)
+lemma eVariationOn_id_Icc (a b : ℝ) :
+    eVariationOn id (Icc a b) = ENNReal.ofReal (b - a) := by
+  simpa using eVariationOn_id (s := univ) (by simp) (by simp)
 
 /-- The identity function has bounded variation on every interval `Icc a b`. -/
 @[simp]
-lemma BoundedVariationOn.id_Icc {a b : ℝ} : BoundedVariationOn id (.Icc a b) := by
+lemma BoundedVariationOn.id_Icc (a b : ℝ) : BoundedVariationOn id (Icc a b) := by
   rcases lt_or_ge b a with hab | hab <;> simp [hab, BoundedVariationOn, eVariationOn_id_Icc]
 
 /-! ### Lipschitz functions and bounded variation -/

From e70358fb9791ee6d4f308ac839e804fe2bdfa6a0 Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:42:29 -0700
Subject: [PATCH 15/26] eliminated BoundedVariationOn.of_subsingleton as
 redundant

---
 .../EMetricSpace/BoundedVariation.lean        | 102 +++++++++---------
 1 file changed, 50 insertions(+), 52 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index e42c44e733e0a2..a78b7c48f6fbe8 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -220,10 +220,6 @@ protected theorem subsingleton (f : α → E) {s : Set α} (hs : s.Subsingleton)
     eVariationOn f s = 0 :=
   constant_on (hs.image f)
 
-/-- A function has bounded variation on any subsingleton set. -/
-lemma _root_.BoundedVariationOn.of_subsingleton {f : α → E} {s : Set α} (h : s.Subsingleton) :
-    BoundedVariationOn f s := by simp [BoundedVariationOn, h]
-
 theorem lowerSemicontinuous_aux {ι : Type*} {F : ι → α → E} {p : Filter ι} {f : α → E} {s : Set α}
     (Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))) {v : ℝ≥0∞} (hv : v < eVariationOn f s) :
     ∀ᶠ n : ι in p, v < eVariationOn (F n) s := by
@@ -484,13 +480,12 @@ the space's distances makes the total variation finite). -/
 theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α → E) (s : Finset α) :
     BoundedVariationOn f s := by
   obtain rfl | hne := s.eq_empty_or_nonempty
-  · simp [BoundedVariationOn.of_subsingleton]
-  let k := s.card
-  have hk : 0 < k := s.card_pos.2 hne
-  let u : ℕ → α := fun n ↦ s.orderEmbOfFin (by rfl : _ = k) ⟨min n (k - 1), by grind⟩
-  have : s = u '' Iic (k - 1) := by
+  · simp [BoundedVariationOn]
+  have := s.card_pos.2 hne
+  let u : ℕ → α := fun n ↦ s.orderEmbOfFin rfl ⟨min n (s.card - 1), by grind⟩
+  have : s = u '' Iic (s.card - 1) := by
     ext
-    simp only [← s.range_orderEmbOfFin (rfl : _ = k), mem_image, mem_Iic, mem_range, u]
+    simp only [← s.range_orderEmbOfFin rfl, mem_image, mem_Iic, mem_range, u]
     constructor
     · rintro ⟨i, rfl⟩; exact ⟨i.val, by grind⟩
     · rintro ⟨i, hi, rfl⟩; use ⟨i, by omega⟩; congr; omega
@@ -1166,72 +1161,75 @@ theorem _root_.BoundedVariationOn.tendsto_atBot_limUnder [CompleteSpace E] [hE :
 
 end eVariationOn
 
+section Monotone
+
 /-! ### Variation of monotone functions -/
 
-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) := by
-  apply iSup_le _
-  rintro ⟨n, ⟨u, hu, us⟩⟩
-  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)
-
-theorem MonotoneOn.locallyBoundedVariationOn {f : α → ℝ} {s : Set α} (hf : MonotoneOn f s) :
-    LocallyBoundedVariationOn f s := fun _ _ as bs =>
-  ((hf.eVariationOn_le as bs).trans_lt ENNReal.ofReal_lt_top).ne
+open ENNReal Finset
 
-theorem MonotoneOn.boundedVariationOn
-    {f : α → ℝ} {s : Set α} {C : ℝ} (hf : MonotoneOn f s) (h : ∀ x ∈ s, |f x| ≤ C) :
-    BoundedVariationOn f s := by
-  suffices eVariationOn f s ≤ ENNReal.ofReal (2 * C) from
-    ne_of_lt (this.trans_lt (by simp [ENNReal.mul_lt_top]))
-  rw [eVariationOn.eq_biSup_inter_Icc]
-  simp only [mem_setOf_eq, iSup_le_iff, and_imp, Prod.forall]
-  intro a b as bs hab
-  grw [hf.eVariationOn_le as bs]
-  exact ENNReal.ofReal_mono (by grind)
+variable {f : α → ℝ} {s : Set α} {C : ℝ} {a b : α}
 
 /-- The variation of a monotone real-valued function on `s ∩ Icc a b` equals its increment
 `f b - f a`. -/
-theorem MonotoneOn.eVariationOn_eq {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) := by
+theorem MonotoneOn.eVariationOn_eq (hf : MonotoneOn f s) (as : a ∈ s) (bs : b ∈ s) :
+    eVariationOn f (s ∩ Icc a b) = .ofReal (f b - f a) := by
+  have hle : eVariationOn f (s ∩ Icc a b) ≤ .ofReal (f b - f a) := by
+    apply iSup_le _
+    rintro ⟨n, ⟨u, hu, us⟩⟩
+    calc
+      _ = ∑ i ∈ range n, .ofReal (f (u (i + 1)) - f (u i)) := by
+        refine 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 _)))
+      _ = .ofReal (∑ i ∈ range n, (f (u (i + 1)) - f (u i))) := by
+        rw [ofReal_sum_of_nonneg]
+        exact fun i _ ↦ sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
+      _ = .ofReal (f (u n) - f (u 0)) := by rw [sum_range_sub (f <| u ·)]
+      _ ≤ _ :=
+        ofReal_le_ofReal (sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1))
   rcases le_or_gt a b with hab | hab
-  · have h : BoundedVariationOn f (s ∩ Icc a b) := hf.locallyBoundedVariationOn a b as bs
-    apply eq_of_le_of_ge (eVariationOn_le hf as bs) (ENNReal.ofReal_le_of_le_toReal _)
+  · have h : BoundedVariationOn f (s ∩ Icc a b) := (hle.trans_lt ofReal_lt_top).ne
+    apply eq_of_le_of_ge hle (ofReal_le_of_le_toReal _)
     grw [← h.dist_le (x := a) (y := b)] <;> grind [Real.dist_eq]
   · simp [hab, hf bs as hab.le]
 
+theorem MonotoneOn.locallyBoundedVariationOn (hf : MonotoneOn f s) :
+    LocallyBoundedVariationOn f s := fun _ _ as bs =>
+  ((hf.eVariationOn_eq as bs).le.trans_lt ofReal_lt_top).ne
+
+theorem MonotoneOn.boundedVariationOn (hf : MonotoneOn f s) (h : ∀ x ∈ s, |f x| ≤ C) :
+    BoundedVariationOn f s := by
+  suffices eVariationOn f s ≤ .ofReal (2 * C) from
+    ne_of_lt (this.trans_lt (by simp [mul_lt_top]))
+  rw [eVariationOn.eq_biSup_inter_Icc]
+  simp only [mem_setOf_eq, iSup_le_iff, and_imp, Prod.forall]
+  intro a b as bs hab
+  grw [(hf.eVariationOn_eq as bs).le]
+  exact ofReal_mono (by grind)
+
+@[deprecated MonotoneOn.eVariationOn_eq (since := "2026-07-08")]
+theorem MonotoneOn.eVariationOn_le (hf : MonotoneOn f s) (as : a ∈ s) (bs : b ∈ s) :
+    eVariationOn f (s ∩ Icc a b) ≤ .ofReal (f b - f a) := (hf.eVariationOn_eq as bs).le
+
 /-- The variation of the identity on `s ∩ Icc a b` is `b - a`. -/
 lemma eVariationOn_id {a b : ℝ} {s : Set ℝ} (as : a ∈ s) (bs : b ∈ s) :
-    eVariationOn id (s ∩ Icc a b) = ENNReal.ofReal (b - a) :=
+    eVariationOn id (s ∩ Icc a b) = .ofReal (b - a) :=
   (monotone_id.monotoneOn _).eVariationOn_eq as bs
 
 /-- The variation of the identity on `Icc a b` is `b - a`. -/
 @[simp]
-lemma eVariationOn_id_Icc (a b : ℝ) :
-    eVariationOn id (Icc a b) = ENNReal.ofReal (b - a) := by
+lemma eVariationOn_id_Icc (a b : ℝ) : eVariationOn id (Icc a b) = .ofReal (b - a) := by
   simpa using eVariationOn_id (s := univ) (by simp) (by simp)
 
 /-- The identity function has bounded variation on every interval `Icc a b`. -/
 @[simp]
 lemma BoundedVariationOn.id_Icc (a b : ℝ) : BoundedVariationOn id (Icc a b) := by
-  rcases lt_or_ge b a with hab | hab <;> simp [hab, BoundedVariationOn, eVariationOn_id_Icc]
+  simp [BoundedVariationOn]
 
 /-! ### Lipschitz functions and bounded variation -/
 
+end Monotone
 section LipschitzOnWith
 
 variable {F : Type*} [PseudoEMetricSpace F]

From 7eadf53faf61ef12b8c00e1f46159859c8e91aac Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:45:10 -0700
Subject: [PATCH 16/26] make BoundedVariationOn.of_finset private as it is
 superseded by BoundedVariationOn.of_finite

---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index a78b7c48f6fbe8..67a81f2836768f 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -475,10 +475,8 @@ theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u
       · simp [IsLeast, hu n.le_succ]
     _ = _ := by simp [Finset.sum_range_succ, ih]
 
-/-- A function valued in a metric space has bounded variation on any `Finset` (the finiteness of
-the space's distances makes the total variation finite). -/
-theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α → E) (s : Finset α) :
-    BoundedVariationOn f s := by
+private theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α → E)
+    (s : Finset α) : BoundedVariationOn f s := by
   obtain rfl | hne := s.eq_empty_or_nonempty
   · simp [BoundedVariationOn]
   have := s.card_pos.2 hne
@@ -492,7 +490,8 @@ theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α 
   have hmono : Monotone u := fun _ _ _ ↦ OrderEmbedding.monotone _ (by grind)
   simp [BoundedVariationOn, this, image_range_of_monotone f hmono _]
 
-/-- A version of the previous theorem for `Finite` sets. -/
+/-- A function valued in a metric space has bounded variation on any `Finset` (the finiteness of
+the space's distances makes the total variation finite). -/
 @[simp]
 theorem _root_.BoundedVariationOn.of_finite {E} [PseudoMetricSpace E] (f : α → E) (s : Set α)
 [Finite s] : BoundedVariationOn f s := by

From 938ee1a6727d73ff3b278a6dc375ac80313799c2 Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 10:46:51 -0700
Subject: [PATCH 17/26] Apply suggestion from @CoolRmal

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 67a81f2836768f..f263b7a91d13fb 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -469,9 +469,7 @@ theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u
     _ = eVariationOn f (u '' Iic n ∪ {u n, u (n + 1)}) := by congr; grind
     _ = eVariationOn f (u '' Iic n) + eVariationOn f {u n, u (n + 1)} := by
       apply union f (x := u n) _ _
-      · simp only [IsGreatest, mem_image, mem_Iic, mem_upperBounds, forall_exists_index, and_imp,
-        forall_apply_eq_imp_iff₂]
-        refine ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
+      · simpa [IsGreatest, upperBounds] using ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
       · simp [IsLeast, hu n.le_succ]
     _ = _ := by simp [Finset.sum_range_succ, ih]
 

From fffd2fba9ba6a382a76b76fb567e75b8bfe01eae Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 11:02:56 -0700
Subject: [PATCH 18/26] golf

---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index f263b7a91d13fb..30cd04acc906ba 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -450,14 +450,9 @@ theorem union' (f : α → E) {s t : Set α} {x y : α} (hs : IsGreatest s x) (h
     (hxy : x ≤ y) :
     eVariationOn f (s ∪ t) = eVariationOn f s + edist (f x) (f y) + eVariationOn f t := calc
   _ = eVariationOn f ((s ∪ {x, y}) ∪ t) := by congr 1; grind [hs.1, ht.1]
-  _ = eVariationOn f (s ∪ {x, y}) + eVariationOn f t := by
-    apply union f _ ht
-    simp [IsGreatest, hxy, upperBounds_mono_mem hxy hs.2]
-  _ = eVariationOn f s + eVariationOn f {x, y} + eVariationOn f t := by
-    congr
-    apply union f hs _
-    simp [IsLeast, hxy]
-  _ = _ := by simp [pair]
+  _ = _ := by
+    rw [union f _ ht, union f hs _]
+    <;> simp [IsLeast, IsGreatest, hxy, upperBounds_mono_mem hxy hs.2]
 
 /-- The variation of `f` along the image of `{0, …, n}` under a monotone sequence `u` is the sum of
 the distances between consecutive values. -/

From 6b610a6fd13ec4a9cc854befd6a5f501423a8f0d Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 11:07:30 -0700
Subject: [PATCH 19/26] more golf

---
 .../Topology/EMetricSpace/BoundedVariation.lean    | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 30cd04acc906ba..9c3109fff21b73 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -438,10 +438,10 @@ theorem pair (f : α → E) (a b : α) : eVariationOn f {a, b} = edist (f a) (f
     rintro ⟨n, u, hmono, hi⟩
     rcases (by omega : n = 0 ∨ n = 1 ∨ 2 ≤ n) with rfl | rfl | hn
     · simp
-    · have : u 0 < u 1 := hmono (by simp) (by simp) zero_lt_one
+    · have := hmono (by simp) (by simp) zero_lt_one
       simp [(by grind : u 0 = a), (by grind : u 1 = b), edist_comm]
-    · have : u 0 < u 1 := hmono (by simp) (by grind) zero_lt_one
-      have : u 1 < u 2 := hmono (by grind) (by grind) one_lt_two
+    · have := hmono (by simp) (by grind) zero_lt_one
+      have := hmono (by grind) (by grind) one_lt_two
       grind
 
 /-- A generalization of `eVariationOn.union` in which the greatest element of `s` is allowed to lie
@@ -451,7 +451,7 @@ theorem union' (f : α → E) {s t : Set α} {x y : α} (hs : IsGreatest s x) (h
     eVariationOn f (s ∪ t) = eVariationOn f s + edist (f x) (f y) + eVariationOn f t := calc
   _ = eVariationOn f ((s ∪ {x, y}) ∪ t) := by congr 1; grind [hs.1, ht.1]
   _ = _ := by
-    rw [union f _ ht, union f hs _]
+    rw [union f _ ht, union f hs]
     <;> simp [IsLeast, IsGreatest, hxy, upperBounds_mono_mem hxy hs.2]
 
 /-- The variation of `f` along the image of `{0, …, n}` under a monotone sequence `u` is the sum of
@@ -462,11 +462,11 @@ theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u
   | zero => simp [Iic]
   | succ n ih => calc
     _ = eVariationOn f (u '' Iic n ∪ {u n, u (n + 1)}) := by congr; grind
-    _ = eVariationOn f (u '' Iic n) + eVariationOn f {u n, u (n + 1)} := by
-      apply union f (x := u n) _ _
+    _ = _ := by
+      rw [union f (x := u n)]
+      · simp [Finset.sum_range_succ, ih]
       · simpa [IsGreatest, upperBounds] using ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
       · simp [IsLeast, hu n.le_succ]
-    _ = _ := by simp [Finset.sum_range_succ, ih]
 
 private theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α → E)
     (s : Finset α) : BoundedVariationOn f s := by

From 4b1fbfdb99a23e1efac16f506b121d63f8339a1a Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 11:11:44 -0700
Subject: [PATCH 20/26] more golf

---
 .../Topology/EMetricSpace/BoundedVariation.lean    | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 9c3109fff21b73..3d51995fd3aa83 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -448,11 +448,9 @@ theorem pair (f : α → E) (a b : α) : eVariationOn f {a, b} = edist (f a) (f
 to the left of the least element of `t`. -/
 theorem union' (f : α → E) {s t : Set α} {x y : α} (hs : IsGreatest s x) (ht : IsLeast t y)
     (hxy : x ≤ y) :
-    eVariationOn f (s ∪ t) = eVariationOn f s + edist (f x) (f y) + eVariationOn f t := calc
-  _ = eVariationOn f ((s ∪ {x, y}) ∪ t) := by congr 1; grind [hs.1, ht.1]
-  _ = _ := by
-    rw [union f _ ht, union f hs]
-    <;> simp [IsLeast, IsGreatest, hxy, upperBounds_mono_mem hxy hs.2]
+    eVariationOn f (s ∪ t) = eVariationOn f s + edist (f x) (f y) + eVariationOn f t := by
+  rw [(by grind [hs.1, ht.1] : s ∪ t = (s ∪ {x, y}) ∪ t), union f _ ht, union f hs]
+  <;> simp [IsLeast, IsGreatest, hxy, upperBounds_mono_mem hxy hs.2]
 
 /-- The variation of `f` along the image of `{0, …, n}` under a monotone sequence `u` is the sum of
 the distances between consecutive values. -/
@@ -460,10 +458,8 @@ theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u
     eVariationOn f (u '' Iic n) = ∑ i ∈ .range n, edist (f (u i)) (f (u (i + 1))) := by
   induction n with
   | zero => simp [Iic]
-  | succ n ih => calc
-    _ = eVariationOn f (u '' Iic n ∪ {u n, u (n + 1)}) := by congr; grind
-    _ = _ := by
-      rw [union f (x := u n)]
+  | succ n ih =>
+      rw [(by grind : u '' Iic (n + 1) = u '' Iic n ∪ {u n, u (n + 1)}), union f (x := u n)]
       · simp [Finset.sum_range_succ, ih]
       · simpa [IsGreatest, upperBounds] using ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
       · simp [IsLeast, hu n.le_succ]

From 1df8b21fc483a2791ed1169f3c55956c3879f708 Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 11:17:06 -0700
Subject: [PATCH 21/26] golf

---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 3d51995fd3aa83..0e87e1cdb060a5 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -407,7 +407,7 @@ theorem sum (f : α → E) {s : Set α} {E : ℕ → α} (hE : Monotone E) {n :
     ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) =
       eVariationOn f (s ∩ Icc (E 0) (E n)) := by
   induction n with
-  | zero => simp [eVariationOn.subsingleton f Subsingleton.inter_singleton]
+  | zero => simp [Subsingleton.inter_singleton]
   | succ n ih =>
     by_cases hn₀ : n = 0
     · simp [hn₀]

From 84bcce9e1abd37f3ffd5e8ffd90b3a41f4a7c5d6 Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 22:15:34 -0700
Subject: [PATCH 22/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 0e87e1cdb060a5..5305a726d0d2a6 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -487,6 +487,7 @@ theorem _root_.BoundedVariationOn.of_finite {E} [PseudoMetricSpace E] (f : α 
   simpa using BoundedVariationOn.of_finset f s.toFinite.toFinset
 
 /-! ### Composition of bounded variation functions with monotone functions -/
+
 section Monotone
 
 variable {β : Type*} [LinearOrder β]

From 06e99b351de3105e070ce98e67f7f980dc136e2a Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 22:15:54 -0700
Subject: [PATCH 23/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 5305a726d0d2a6..19b8402f3a355f 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -1216,9 +1216,10 @@ lemma eVariationOn_id_Icc (a b : ℝ) : eVariationOn id (Icc a b) = .ofReal (b -
 lemma BoundedVariationOn.id_Icc (a b : ℝ) : BoundedVariationOn id (Icc a b) := by
   simp [BoundedVariationOn]
 
+end Monotone
+
 /-! ### Lipschitz functions and bounded variation -/
 
-end Monotone
 section LipschitzOnWith
 
 variable {F : Type*} [PseudoEMetricSpace F]

From c4a55bd0775996042f5ab63cd81d35f7d32b783f Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 22:16:21 -0700
Subject: [PATCH 24/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 .../EMetricSpace/BoundedVariation.lean        | 32 +++++++++----------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 19b8402f3a355f..55152b27411867 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -1162,23 +1162,23 @@ variable {f : α → ℝ} {s : Set α} {C : ℝ} {a b : α}
 `f b - f a`. -/
 theorem MonotoneOn.eVariationOn_eq (hf : MonotoneOn f s) (as : a ∈ s) (bs : b ∈ s) :
     eVariationOn f (s ∩ Icc a b) = .ofReal (f b - f a) := by
-  have hle : eVariationOn f (s ∩ Icc a b) ≤ .ofReal (f b - f a) := by
-    apply iSup_le _
-    rintro ⟨n, ⟨u, hu, us⟩⟩
-    calc
-      _ = ∑ i ∈ range n, .ofReal (f (u (i + 1)) - f (u i)) := by
-        refine 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 _)))
-      _ = .ofReal (∑ i ∈ range n, (f (u (i + 1)) - f (u i))) := by
-        rw [ofReal_sum_of_nonneg]
-        exact fun i _ ↦ sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
-      _ = .ofReal (f (u n) - f (u 0)) := by rw [sum_range_sub (f <| u ·)]
-      _ ≤ _ :=
-        ofReal_le_ofReal (sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1))
   rcases le_or_gt a b with hab | hab
-  · have h : BoundedVariationOn f (s ∩ Icc a b) := (hle.trans_lt ofReal_lt_top).ne
+  · have hle : eVariationOn f (s ∩ Icc a b) ≤ .ofReal (f b - f a) := by
+      apply iSup_le _
+      rintro ⟨n, ⟨u, hu, us⟩⟩
+      calc
+        _ = ∑ i ∈ range n, .ofReal (f (u (i + 1)) - f (u i)) := by
+          refine 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 _)))
+        _ = .ofReal (∑ i ∈ range n, (f (u (i + 1)) - f (u i))) := by
+          rw [ofReal_sum_of_nonneg]
+          exact fun i _ ↦ sub_nonneg_of_le (hf (us i).1 (us (i + 1)).1 (hu (Nat.le_succ _)))
+        _ = .ofReal (f (u n) - f (u 0)) := by rw [sum_range_sub (f <| u ·)]
+        _ ≤ _ :=
+          ofReal_le_ofReal (sub_le_sub (hf (us n).1 bs (us n).2.2) (hf as (us 0).1 (us 0).2.1))
+    have h : BoundedVariationOn f (s ∩ Icc a b) := (hle.trans_lt ofReal_lt_top).ne
     apply eq_of_le_of_ge hle (ofReal_le_of_le_toReal _)
     grw [← h.dist_le (x := a) (y := b)] <;> grind [Real.dist_eq]
   · simp [hab, hf bs as hab.le]

From dfd4810159228bed6d48875709da19ccaad546ec Mon Sep 17 00:00:00 2001
From: teorth <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 22:16:49 -0700
Subject: [PATCH 25/26] Update
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 55152b27411867..25405aee26a5dc 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -459,10 +459,10 @@ theorem image_range_of_monotone (f : α → E) {u : ℕ → α} (hu : Monotone u
   induction n with
   | zero => simp [Iic]
   | succ n ih =>
-      rw [(by grind : u '' Iic (n + 1) = u '' Iic n ∪ {u n, u (n + 1)}), union f (x := u n)]
-      · simp [Finset.sum_range_succ, ih]
-      · simpa [IsGreatest, upperBounds] using ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
-      · simp [IsLeast, hu n.le_succ]
+    rw [(by grind : u '' Iic (n + 1) = u '' Iic n ∪ {u n, u (n + 1)}), union f]
+    · simp [Finset.sum_range_succ, ih]
+    · simpa [IsGreatest, upperBounds] using ⟨⟨n, by simp⟩, fun a ha ↦ hu ha⟩
+    · simp [IsLeast, hu n.le_succ]
 
 private theorem _root_.BoundedVariationOn.of_finset {E} [PseudoMetricSpace E] (f : α → E)
     (s : Finset α) : BoundedVariationOn f s := by

From e74f9ee2602ee3f9c7ad3ed727fae58642550a9d Mon Sep 17 00:00:00 2001
From: Terence Tao <tao@math.ucla.edu>
Date: Thu, 9 Jul 2026 22:31:26 -0700
Subject: [PATCH 26/26] final reviewer request and last-minute golf

---
 Mathlib/Topology/EMetricSpace/BoundedVariation.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 25405aee26a5dc..c643d5d3a848db 100644
--- a/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -1183,9 +1183,13 @@ theorem MonotoneOn.eVariationOn_eq (hf : MonotoneOn f s) (as : a ∈ s) (bs : b
     grw [← h.dist_le (x := a) (y := b)] <;> grind [Real.dist_eq]
   · simp [hab, hf bs as hab.le]
 
+@[deprecated MonotoneOn.eVariationOn_eq (since := "2026-07-08")]
+theorem MonotoneOn.eVariationOn_le (hf : MonotoneOn f s) (as : a ∈ s) (bs : b ∈ s) :
+    eVariationOn f (s ∩ Icc a b) ≤ .ofReal (f b - f a) := (hf.eVariationOn_eq as bs).le
+
 theorem MonotoneOn.locallyBoundedVariationOn (hf : MonotoneOn f s) :
     LocallyBoundedVariationOn f s := fun _ _ as bs =>
-  ((hf.eVariationOn_eq as bs).le.trans_lt ofReal_lt_top).ne
+  ((hf.eVariationOn_eq as bs) ▸ ofReal_lt_top).ne
 
 theorem MonotoneOn.boundedVariationOn (hf : MonotoneOn f s) (h : ∀ x ∈ s, |f x| ≤ C) :
     BoundedVariationOn f s := by
@@ -1194,13 +1198,9 @@ theorem MonotoneOn.boundedVariationOn (hf : MonotoneOn f s) (h : ∀ x ∈ s, |f
   rw [eVariationOn.eq_biSup_inter_Icc]
   simp only [mem_setOf_eq, iSup_le_iff, and_imp, Prod.forall]
   intro a b as bs hab
-  grw [(hf.eVariationOn_eq as bs).le]
+  grw [hf.eVariationOn_eq as bs]
   exact ofReal_mono (by grind)
 
-@[deprecated MonotoneOn.eVariationOn_eq (since := "2026-07-08")]
-theorem MonotoneOn.eVariationOn_le (hf : MonotoneOn f s) (as : a ∈ s) (bs : b ∈ s) :
-    eVariationOn f (s ∩ Icc a b) ≤ .ofReal (f b - f a) := (hf.eVariationOn_eq as bs).le
-
 /-- The variation of the identity on `s ∩ Icc a b` is `b - a`. -/
 lemma eVariationOn_id {a b : ℝ} {s : Set ℝ} (as : a ∈ s) (bs : b ∈ s) :
     eVariationOn id (s ∩ Icc a b) = .ofReal (b - a) :=