From 2043b82d6f032f485719a208f35a915d498857af Mon Sep 17 00:00:00 2001
From: yuanyi-350 <kysyy1@126.com>
Date: Thu, 16 Apr 2026 20:22:10 +0800
Subject: [PATCH 1/3] refactor: golf LpSeminorm/Count, Pi, ProductMeasure

---
 Mathlib/MeasureTheory/Constructions/Pi.lean   | 23 +++++--------------
 .../Function/LpSeminorm/Count.lean            | 21 +++++++----------
 Mathlib/Probability/ProductMeasure.lean       |  2 +-
 3 files changed, 15 insertions(+), 31 deletions(-)

diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean
index 5f0f7f9209e3a2..1ad00cb7d6a5b2 100644
--- a/Mathlib/MeasureTheory/Constructions/Pi.lean
+++ b/Mathlib/MeasureTheory/Constructions/Pi.lean
@@ -450,23 +450,6 @@ theorem ae_eq_set_pi {I : Set ι} {s t : ∀ i, Set (α i)} (h : ∀ i ∈ I, s
     Set.pi I s =ᵐ[Measure.pi μ] Set.pi I t :=
   (ae_le_set_pi fun i hi => (h i hi).le).antisymm (ae_le_set_pi fun i hi => (h i hi).symm.le)
 
-lemma pi_map_piCongrLeft [hι' : Fintype ι'] (e : ι ≃ ι') {β : ι' → Type*}
-    [∀ i, MeasurableSpace (β i)] (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] :
-    (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e)
-      = Measure.pi μ := by
-  let e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) :=
-    MeasurableEquiv.piCongrLeft (fun i ↦ β i) e
-  refine Measure.pi_eq (fun s _ ↦ ?_) |>.symm
-  rw [e_meas.measurableEmbedding.map_apply]
-  let s' : (i : ι) → Set (β (e i)) := fun i ↦ s (e i)
-  have : e_meas ⁻¹' pi univ s = pi univ s' := by
-    ext x
-    simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, s']
-    refine (e.forall_congr ?_).symm
-    intro i
-    rw [MeasurableEquiv.piCongrLeft_apply_apply e x i]
-  simpa [this] using Fintype.prod_equiv _ (fun _ ↦ (μ _) (s' _)) _ (congrFun rfl)
-
 lemma pi_map_piOptionEquivProd {β : Option ι → Type*} [∀ i, MeasurableSpace (β i)]
     (μ : (i : Option ι) → Measure (β i)) [∀ (i : Option ι), SigmaFinite (μ i)] :
     ((Measure.pi fun i ↦ μ (some i)).prod (μ none)).map
@@ -755,6 +738,12 @@ theorem volume_measurePreserving_piCongrLeft (α : ι → Type*) (f : ι' ≃ ι
     MeasurePreserving (MeasurableEquiv.piCongrLeft α f) volume volume :=
   measurePreserving_piCongrLeft (fun _ ↦ volume) f
 
+lemma pi_map_piCongrLeft (e : ι ≃ ι') {β : ι' → Type*} [∀ i, MeasurableSpace (β i)]
+    (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] :
+    (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e) =
+      Measure.pi μ :=
+  (measurePreserving_piCongrLeft (α := fun i ↦ β i) (μ := μ) e).map_eq
+
 theorem measurePreserving_arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α]
     [MeasurableSpace β] [Fintype γ] (μ : γ → Measure α) (ν : γ → Measure β) [∀ i, SigmaFinite (μ i)]
     [∀ i, SigmaFinite (ν i)] :
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
index 57377f7cec7370..6b18736ed9916d 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
@@ -34,22 +34,17 @@ lemma enorm_le_eLpNorm_count (f : α → ε) (i : α) (hp : p ≠ 0) :
       _ = eLpNorm f p (count.restrict {i}) := by simp
       _ ≤ eLpNorm f p count := eLpNorm_restrict_le ..
 
+omit [MeasurableSingletonClass α] in
 lemma eLpNorm_count_lt_top_of_lt [Finite α] (h : ∀ i, ‖f i‖ₑ < ∞) :
     eLpNorm f p .count < ∞ := by
   letI _ := Fintype.ofFinite α
-  simp_rw [eLpNorm]
-  split_ifs with h2 h3
-  · exact ENNReal.zero_lt_top
-  · refine (essSup_le_of_ae_le (Finset.univ.sup (‖f ·‖ₑ)) ?_).trans_lt ?_
-    · filter_upwards with x
-      exact Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ _)
-    · simp_rw [Finset.sup_lt_iff ENNReal.zero_lt_top, h, implies_true]
-  · refine (ENNReal.rpow_lt_top_iff_of_pos ?_).mpr ?_
-    · rw [one_div, inv_pos]
-      exact ENNReal.toReal_pos h2 h3
-    · simp_rw [lintegral_count, tsum_eq_sum (s := Finset.univ) (by simp), ENNReal.sum_lt_top,
-        Finset.mem_univ, forall_const, ENNReal.rpow_lt_top_iff_of_pos (ENNReal.toReal_pos h2 h3), h,
-        implies_true]
+  let C : ℝ≥0∞ := Finset.univ.sup (‖f ·‖ₑ)
+  have hC : ∀ x, ‖f x‖ₑ ≤ C := fun x => Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)
+  have hC_lt : C < ∞ := by
+    simp [C, Finset.sup_lt_iff, h]
+  refine (eLpNorm_mono_enorm (μ := (count : Measure α)) (p := p) (f := f)
+    (g := fun _ : α => C) fun x => by simpa [C] using hC x).trans_lt ?_
+  exact (memLp_const_enorm (μ := (count : Measure α)) (p := p) (c := C) hC_lt.ne).eLpNorm_lt_top
 
 lemma eLpNorm_count_lt_top [Finite α] (hp : p ≠ 0) :
     eLpNorm f p .count < ∞ ↔ ∀ i, ‖f i‖ₑ < ∞ :=
diff --git a/Mathlib/Probability/ProductMeasure.lean b/Mathlib/Probability/ProductMeasure.lean
index 49333de91686c9..9a1e464c9ede56 100644
--- a/Mathlib/Probability/ProductMeasure.lean
+++ b/Mathlib/Probability/ProductMeasure.lean
@@ -89,7 +89,7 @@ theorem piContent_eq_measure_pi [Fintype ι] {s : Set (Π i, X i)} (hs : Measura
   have : s = cylinder univ (MeasurableEquiv.piCongrLeft X e ⁻¹' s) := rfl
   nth_rw 1 [this]
   dsimp [e]
-  rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← Measure.pi_map_piCongrLeft e,
+  rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← MeasureTheory.pi_map_piCongrLeft e,
     ← Measure.map_apply (by fun_prop) hs]; rfl
 
 end Preliminaries

From fdd51c2cd79e35daad2e5caa4d6145c43f2fc163 Mon Sep 17 00:00:00 2001
From: "Yi.Yuan" <kysyy1@126.com>
Date: Thu, 16 Apr 2026 22:30:50 +0800
Subject: [PATCH 2/3] golf

---
 .../MeasureTheory/Function/LpSeminorm/Count.lean  | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
index 6b18736ed9916d..2a0bc5f6d11632 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
@@ -35,16 +35,13 @@ lemma enorm_le_eLpNorm_count (f : α → ε) (i : α) (hp : p ≠ 0) :
       _ ≤ eLpNorm f p count := eLpNorm_restrict_le ..
 
 omit [MeasurableSingletonClass α] in
-lemma eLpNorm_count_lt_top_of_lt [Finite α] (h : ∀ i, ‖f i‖ₑ < ∞) :
-    eLpNorm f p .count < ∞ := by
-  letI _ := Fintype.ofFinite α
+lemma eLpNorm_count_lt_top_of_lt [Finite α] (h : ∀ i, ‖f i‖ₑ < ∞) : eLpNorm f p .count < ∞ := by
+  haveI := Fintype.ofFinite α
   let C : ℝ≥0∞ := Finset.univ.sup (‖f ·‖ₑ)
-  have hC : ∀ x, ‖f x‖ₑ ≤ C := fun x => Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)
-  have hC_lt : C < ∞ := by
-    simp [C, Finset.sup_lt_iff, h]
-  refine (eLpNorm_mono_enorm (μ := (count : Measure α)) (p := p) (f := f)
-    (g := fun _ : α => C) fun x => by simpa [C] using hC x).trans_lt ?_
-  exact (memLp_const_enorm (μ := (count : Measure α)) (p := p) (c := C) hC_lt.ne).eLpNorm_lt_top
+  have hC : ∀ x, ‖f x‖ₑ ≤ C := fun x ↦ Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)
+  have hC_lt : C < ∞ := by simp [C, h]
+  exact (eLpNorm_mono_enorm (g := fun _ ↦ C) fun x => by simp [hC x]).trans_lt
+    (memLp_const_enorm hC_lt.ne).eLpNorm_lt_top
 
 lemma eLpNorm_count_lt_top [Finite α] (hp : p ≠ 0) :
     eLpNorm f p .count < ∞ ↔ ∀ i, ‖f i‖ₑ < ∞ :=

From fbeeab2a96a3a812f58970d9d7d49d2880818d85 Mon Sep 17 00:00:00 2001
From: "Yi.Yuan" <kysyy1@126.com>
Date: Thu, 16 Apr 2026 23:02:15 +0800
Subject: [PATCH 3/3] golf

---
 Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
index 2a0bc5f6d11632..6569b5227b6c59 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
@@ -37,11 +37,9 @@ lemma enorm_le_eLpNorm_count (f : α → ε) (i : α) (hp : p ≠ 0) :
 omit [MeasurableSingletonClass α] in
 lemma eLpNorm_count_lt_top_of_lt [Finite α] (h : ∀ i, ‖f i‖ₑ < ∞) : eLpNorm f p .count < ∞ := by
   haveI := Fintype.ofFinite α
-  let C : ℝ≥0∞ := Finset.univ.sup (‖f ·‖ₑ)
-  have hC : ∀ x, ‖f x‖ₑ ≤ C := fun x ↦ Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)
-  have hC_lt : C < ∞ := by simp [C, h]
-  exact (eLpNorm_mono_enorm (g := fun _ ↦ C) fun x => by simp [hC x]).trans_lt
-    (memLp_const_enorm hC_lt.ne).eLpNorm_lt_top
+  refine (eLpNorm_mono_enorm (g := fun _ ↦ Finset.univ.sup (‖f ·‖ₑ)) ?_).trans_lt ?_
+  · exact fun x ↦ Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)
+  · exact (memLp_const_enorm <| by simp [h, LT.lt.ne]).eLpNorm_lt_top
 
 lemma eLpNorm_count_lt_top [Finite α] (hp : p ≠ 0) :
     eLpNorm f p .count < ∞ ↔ ∀ i, ‖f i‖ₑ < ∞ :=