From 8b918ffac212de42eb7d7d9a16fd5083337ed2ae Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Mon, 15 May 2023 16:16:29 +0200
Subject: [PATCH 1/2] mathport

---
 .../MeasureTheory/Measure/MeasureSpace.lean   | 17 ++++++++++-
 .../MeasureTheory/Measure/OuterMeasure.lean   | 28 ++++++++++++++++++-
 2 files changed, 43 insertions(+), 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index bde646412d437..c528d605fc067 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 
 ! This file was ported from Lean 3 source module measure_theory.measure.measure_space
-! leanprover-community/mathlib commit 88fcb83fe7996142dfcfe7368d31304a9adc874a
+! leanprover-community/mathlib commit 343e80208d29d2d15f8050b929aa50fe4ce71b55
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1058,6 +1058,21 @@ instance instCompleteLattice [MeasurableSpace α] : CompleteLattice (Measure α)
 
 end sInf
 
+@[simp]
+theorem MeasureTheory.OuterMeasure.toMeasure_top [MeasurableSpace α] :
+    (⊤ : OuterMeasure α).toMeasure (by rw [outer_measure.top_caratheodory] <;> exact le_top) =
+      (⊤ : Measure α) :=
+  top_unique fun s hs => by
+    cases' s.eq_empty_or_nonempty with h h <;>
+      simp [h, to_measure_apply ⊤ _ hs, outer_measure.top_apply]
+#align measure_theory.outer_measure.to_measure_top MeasureTheory.OuterMeasure.toMeasure_top
+
+@[simp]
+theorem toOuterMeasure_top [MeasurableSpace α] :
+    (⊤ : Measure α).toOuterMeasure = (⊤ : OuterMeasure α) := by
+  rw [← outer_measure.to_measure_top, to_measure_to_outer_measure, outer_measure.trim_top]
+#align measure_theory.measure.to_outer_measure_top MeasureTheory.Measure.toOuterMeasure_top
+
 @[simp]
 theorem top_add : ⊤ + μ = ⊤ :=
   top_unique <| Measure.le_add_right le_rfl
diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
index c699c1fb9e2b1..5cf8390715971 100644
--- a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 
 ! This file was ported from Lean 3 source module measure_theory.measure.outer_measure
-! leanprover-community/mathlib commit ec4b2eeb50364487f80421c0b4c41328a611f30d
+! leanprover-community/mathlib commit 343e80208d29d2d15f8050b929aa50fe4ce71b55
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -882,6 +882,22 @@ theorem le_bounded_by' {μ : OuterMeasure α} :
   cases' s.eq_empty_or_nonempty with h h <;> simp [h]
 #align measure_theory.outer_measure.le_bounded_by' MeasureTheory.OuterMeasure.le_bounded_by'
 
+@[simp]
+theorem boundedBy_top : boundedBy (⊤ : Set α → ℝ≥0∞) = ⊤ :=
+  by
+  rw [eq_top_iff, le_bounded_by']
+  intro s hs
+  rw [top_apply hs]
+  exact le_rfl
+#align measure_theory.outer_measure.bounded_by_top MeasureTheory.OuterMeasure.boundedBy_top
+
+@[simp]
+theorem boundedBy_zero : boundedBy (0 : Set α → ℝ≥0∞) = 0 :=
+  by
+  rw [← coe_bot, eq_bot_iff]
+  apply bounded_by_le
+#align measure_theory.outer_measure.bounded_by_zero MeasureTheory.OuterMeasure.boundedBy_zero
+
 theorem smul_boundedBy {c : ℝ≥0∞} (hc : c ≠ ∞) : c • boundedBy m = boundedBy (c • m) := by
   simp only [boundedBy , smul_ofFunction hc]
   congr 1 with s : 1
@@ -1334,6 +1350,11 @@ theorem extend_congr {β : Type _} {Pb : β → Prop} {mb : ∀ s : β, Pb s →
   iInf_congr_Prop hP fun _h => hm _ _
 #align measure_theory.extend_congr MeasureTheory.extend_congr
 
+@[simp]
+theorem extend_top {α : Type _} {P : α → Prop} : extend (fun s h => ∞ : ∀ s : α, P s → ℝ≥0∞) = ⊤ :=
+  funext fun x => infᵢ_eq_top.mpr fun i => rfl
+#align measure_theory.extend_top MeasureTheory.extend_top
+
 end Extend
 
 section ExtendSet
@@ -1648,6 +1669,11 @@ theorem trim_trim (m : OuterMeasure α) : m.trim.trim = m.trim :=
   trim_eq_trim_iff.2 fun _s => m.trim_eq
 #align measure_theory.outer_measure.trim_trim MeasureTheory.OuterMeasure.trim_trim
 
+@[simp]
+theorem trim_top : (⊤ : OuterMeasure α).trim = ⊤ :=
+  eq_top_iff.2 <| le_trim _
+#align measure_theory.outer_measure.trim_top MeasureTheory.OuterMeasure.trim_top
+
 @[simp]
 theorem trim_zero : (0 : OuterMeasure α).trim = 0 :=
   ext fun s =>

From 4b50629cd94b6e5b56b17d17f0c3b09e918db359 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Mon, 15 May 2023 16:21:27 +0200
Subject: [PATCH 2/2] Fix

---
 Mathlib/MeasureTheory/Measure/MeasureSpace.lean |  8 ++++----
 Mathlib/MeasureTheory/Measure/OuterMeasure.lean | 12 +++++-------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index c528d605fc067..8aac4dc981874 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -1059,18 +1059,18 @@ instance instCompleteLattice [MeasurableSpace α] : CompleteLattice (Measure α)
 end sInf
 
 @[simp]
-theorem MeasureTheory.OuterMeasure.toMeasure_top [MeasurableSpace α] :
-    (⊤ : OuterMeasure α).toMeasure (by rw [outer_measure.top_caratheodory] <;> exact le_top) =
+theorem _root_.MeasureTheory.OuterMeasure.toMeasure_top [MeasurableSpace α] :
+    (⊤ : OuterMeasure α).toMeasure (by rw [OuterMeasure.top_caratheodory]; exact le_top) =
       (⊤ : Measure α) :=
   top_unique fun s hs => by
     cases' s.eq_empty_or_nonempty with h h <;>
-      simp [h, to_measure_apply ⊤ _ hs, outer_measure.top_apply]
+      simp [h, toMeasure_apply ⊤ _ hs, OuterMeasure.top_apply]
 #align measure_theory.outer_measure.to_measure_top MeasureTheory.OuterMeasure.toMeasure_top
 
 @[simp]
 theorem toOuterMeasure_top [MeasurableSpace α] :
     (⊤ : Measure α).toOuterMeasure = (⊤ : OuterMeasure α) := by
-  rw [← outer_measure.to_measure_top, to_measure_to_outer_measure, outer_measure.trim_top]
+  rw [← OuterMeasure.toMeasure_top, toMeasure_toOuterMeasure, OuterMeasure.trim_top]
 #align measure_theory.measure.to_outer_measure_top MeasureTheory.Measure.toOuterMeasure_top
 
 @[simp]
diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
index 5cf8390715971..d69325a6bd12c 100644
--- a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
@@ -883,8 +883,7 @@ theorem le_bounded_by' {μ : OuterMeasure α} :
 #align measure_theory.outer_measure.le_bounded_by' MeasureTheory.OuterMeasure.le_bounded_by'
 
 @[simp]
-theorem boundedBy_top : boundedBy (⊤ : Set α → ℝ≥0∞) = ⊤ :=
-  by
+theorem boundedBy_top : boundedBy (⊤ : Set α → ℝ≥0∞) = ⊤ := by
   rw [eq_top_iff, le_bounded_by']
   intro s hs
   rw [top_apply hs]
@@ -892,10 +891,9 @@ theorem boundedBy_top : boundedBy (⊤ : Set α → ℝ≥0∞) = ⊤ :=
 #align measure_theory.outer_measure.bounded_by_top MeasureTheory.OuterMeasure.boundedBy_top
 
 @[simp]
-theorem boundedBy_zero : boundedBy (0 : Set α → ℝ≥0∞) = 0 :=
-  by
+theorem boundedBy_zero : boundedBy (0 : Set α → ℝ≥0∞) = 0 := by
   rw [← coe_bot, eq_bot_iff]
-  apply bounded_by_le
+  apply boundedBy_le
 #align measure_theory.outer_measure.bounded_by_zero MeasureTheory.OuterMeasure.boundedBy_zero
 
 theorem smul_boundedBy {c : ℝ≥0∞} (hc : c ≠ ∞) : c • boundedBy m = boundedBy (c • m) := by
@@ -1351,8 +1349,8 @@ theorem extend_congr {β : Type _} {Pb : β → Prop} {mb : ∀ s : β, Pb s →
 #align measure_theory.extend_congr MeasureTheory.extend_congr
 
 @[simp]
-theorem extend_top {α : Type _} {P : α → Prop} : extend (fun s h => ∞ : ∀ s : α, P s → ℝ≥0∞) = ⊤ :=
-  funext fun x => infᵢ_eq_top.mpr fun i => rfl
+theorem extend_top {α : Type _} {P : α → Prop} : extend (fun _ _ => ∞ : ∀ s : α, P s → ℝ≥0∞) = ⊤ :=
+  funext fun _ => iInf_eq_top.mpr fun _ => rfl
 #align measure_theory.extend_top MeasureTheory.extend_top
 
 end Extend