chore: forward-port leanprover-community/mathlib#18983 (#4001)

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 _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, 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 [← OuterMeasure.toMeasure_top, toMeasure_toOuterMeasure, OuterMeasure.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

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,20 @@ 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 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
   simp only [boundedBy , smul_ofFunction hc]
   congr 1 with s : 1
@@ -1334,6 +1348,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 : α, P s → ℝ≥0∞) = ⊤ :=
+  funext fun _ => iInf_eq_top.mpr fun _ => rfl
+#align measure_theory.extend_top MeasureTheory.extend_top
+
 end Extend
 
 section ExtendSet
@@ -1648,6 +1667,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 =>