diff --git a/Carleson/ToMathlib/Analysis/MeanInequalitiesPow.lean b/Carleson/ToMathlib/Analysis/MeanInequalitiesPow.lean
index 957d4cf1b..227b40294 100644
--- a/Carleson/ToMathlib/Analysis/MeanInequalitiesPow.lean
+++ b/Carleson/ToMathlib/Analysis/MeanInequalitiesPow.lean
@@ -1,7 +1,7 @@
 import Mathlib.Analysis.MeanInequalitiesPow
 import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
 
--- Upstreaming status: looks useful and ready to go
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37547
 
 namespace ENNReal
 
diff --git a/Carleson/ToMathlib/Data/ENNReal.lean b/Carleson/ToMathlib/Data/ENNReal.lean
index b4fdda905..328cda83d 100644
--- a/Carleson/ToMathlib/Data/ENNReal.lean
+++ b/Carleson/ToMathlib/Data/ENNReal.lean
@@ -3,8 +3,10 @@ import Mathlib.Analysis.Normed.Group.Uniform
 import Mathlib.Analysis.Normed.Ring.Basic
 import Mathlib.Order.CompletePartialOrder
 
--- Upstreaming status: lemmas seem useful; proofs may need some polish
+-- Upstreaming status: lemmas seem useful; proofs may need some polish.
 -- At least three or four distinct PRs.
+-- `ofReal_inv_le` and `ofReal_div_le` upstreamed in
+-- https://github.com/leanprover-community/mathlib4/pull/37565
 
 /-! ## `ENNReal` manipulation lemmas -/
 
diff --git a/Carleson/ToMathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean b/Carleson/ToMathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
index 161d62a4d..642d69f49 100644
--- a/Carleson/ToMathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
+++ b/Carleson/ToMathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
@@ -2,7 +2,7 @@ import Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
 
 open MeasureTheory
 
--- Upstreaming status: rename to `memLp`, then ready for upstreaming.
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37560
 
 lemma ContinuousMap.memLp {α E : Type*} {m0 : MeasurableSpace α} {p : ENNReal} (μ : Measure α)
     [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E]
diff --git a/Carleson/ToMathlib/MeasureTheory/Function/LpSpace/Indicator.lean b/Carleson/ToMathlib/MeasureTheory/Function/LpSpace/Indicator.lean
index 75969afd7..2393e9061 100644
--- a/Carleson/ToMathlib/MeasureTheory/Function/LpSpace/Indicator.lean
+++ b/Carleson/ToMathlib/MeasureTheory/Function/LpSpace/Indicator.lean
@@ -11,8 +11,7 @@ variable {X : Type*} [TopologicalSpace X] [MeasurableSpace X]
 
 namespace MeasureTheory
 
--- Upstreaming status: seems ready for PRing
--- not actually used in the project, but we want to upstream this and similar lemmas.
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37559
 
 /-- A bounded measurable function with compact support is in L^p. -/
 theorem _root_.HasCompactSupport.memLp_of_enorm_bound {f : X → E} (hf : HasCompactSupport f)
diff --git a/Carleson/ToMathlib/MeasureTheory/Integral/Average.lean b/Carleson/ToMathlib/MeasureTheory/Integral/Average.lean
index 9d1f71349..2e68964e7 100644
--- a/Carleson/ToMathlib/MeasureTheory/Integral/Average.lean
+++ b/Carleson/ToMathlib/MeasureTheory/Integral/Average.lean
@@ -1,6 +1,6 @@
 import Mathlib.MeasureTheory.Integral.Average
 
--- Upstreaming status: useful and good to go
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37551
 
 open MeasureTheory MeasureTheory.Measure Filter Set
 
diff --git a/Carleson/ToMathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean b/Carleson/ToMathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean
index a5e9c2f6e..13d83158e 100644
--- a/Carleson/ToMathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean
+++ b/Carleson/ToMathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean
@@ -3,6 +3,8 @@ import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
 open MeasureTheory
 
 -- Upstreaming status: looks ready for upstreaming; pay attention to the correct file to move to!
+-- `exists_ne_zero_of_setIntegral_ne_zero` and `exists_ne_zero_of_integral_ne_zero` upstreamed in
+-- https://github.com/leanprover-community/mathlib4/pull/37568
 
 -- Put after `setIntegral_re_add_im`
 
diff --git a/Carleson/ToMathlib/MeasureTheory/Integral/IntegrableOn.lean b/Carleson/ToMathlib/MeasureTheory/Integral/IntegrableOn.lean
index ec35c6e3f..db792bef7 100644
--- a/Carleson/ToMathlib/MeasureTheory/Integral/IntegrableOn.lean
+++ b/Carleson/ToMathlib/MeasureTheory/Integral/IntegrableOn.lean
@@ -5,6 +5,9 @@ open Set Filter TopologicalSpace MeasureTheory Function
 open scoped Topology Interval Filter ENNReal MeasureTheory
 
 -- Upstreaming note: Hypotheses and variables have been matched to corresponding Mathlib file
+-- `IntegrableAtFilter.congr` already in mathlib.
+-- `integrableOn_of_integrableOn_inter_support` already in mathlib as
+-- `MeasureTheory.IntegrableOn.of_inter_support`.
 
 variable {α β ε ε' E F : Type*} [MeasurableSpace α]
 
diff --git a/Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean b/Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean
index d170feeae..58ff6bf42 100644
--- a/Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean
+++ b/Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean
@@ -1,6 +1,9 @@
 import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
 
--- Upstreaming status: useful and good to go. Easy generalisations of mathlib lemmas.
+-- Upstreaming status: `lintegral_eq_iSup_eapprox_lintegral'` and `lintegral_comp'`
+-- upstreamed in https://github.com/leanprover-community/mathlib4/pull/37558
+-- Remaining lemmas: shift/scaling aliases, `lintegral_set_mono_fn`
+-- (already `setLIntegral_mono'` in mathlib).
 
 open NNReal ENNReal MeasureTheory Set
 
diff --git a/Carleson/ToMathlib/MeasureTheory/Measure/ENNReal.lean b/Carleson/ToMathlib/MeasureTheory/Measure/ENNReal.lean
index 4fd6eb9ec..7d2ef9546 100644
--- a/Carleson/ToMathlib/MeasureTheory/Measure/ENNReal.lean
+++ b/Carleson/ToMathlib/MeasureTheory/Measure/ENNReal.lean
@@ -1,6 +1,7 @@
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
 
--- Upstreaming status: ready to be upstreamed
+-- Upstreaming status: upstreamed as `measurable_iSup_of_lowerSemicontinuous` (generalized) in
+-- https://github.com/leanprover-community/mathlib4/pull/37552
 
 open Set TopologicalSpace ENNReal
 
diff --git a/Carleson/ToMathlib/Order/LiminfLimsup.lean b/Carleson/ToMathlib/Order/LiminfLimsup.lean
index 8001f59b9..3339eb188 100644
--- a/Carleson/ToMathlib/Order/LiminfLimsup.lean
+++ b/Carleson/ToMathlib/Order/LiminfLimsup.lean
@@ -1,6 +1,6 @@
 import Mathlib.Order.LiminfLimsup
 
--- Upstreaming status: seems like a useful lemma; no obvious clean-up opportunities
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37549
 
 theorem Filter.iSup_liminf_le_liminf_iSup {α β : Type*} {ι : Sort*} [CompleteLattice α]
     {f : Filter β} {u : ι → β → α} :
diff --git a/Carleson/ToMathlib/Topology/Instances/AddCircle/Defs.lean b/Carleson/ToMathlib/Topology/Instances/AddCircle/Defs.lean
index 4d5fd83a3..470064cf4 100644
--- a/Carleson/ToMathlib/Topology/Instances/AddCircle/Defs.lean
+++ b/Carleson/ToMathlib/Topology/Instances/AddCircle/Defs.lean
@@ -2,6 +2,8 @@ import Mathlib.Topology.Instances.AddCircle.Defs
 
 -- Upstreaming status: seems ready to go; lemmas are usually analogues of existing mathlib lemmas
 -- Sometimes, mathlib lemmas need to be renamed along with upstreaming this.
+-- Non-Periodic lemmas upstreamed in
+-- https://github.com/leanprover-community/mathlib4/pull/37570
 
 noncomputable section
 
diff --git a/Carleson/ToMathlib/Topology/Order/Basic.lean b/Carleson/ToMathlib/Topology/Order/Basic.lean
index 094d4e24d..2793229af 100644
--- a/Carleson/ToMathlib/Topology/Order/Basic.lean
+++ b/Carleson/ToMathlib/Topology/Order/Basic.lean
@@ -1,6 +1,7 @@
 import Mathlib.Topology.Order.Basic
 
--- Upstreaming status: perhaps, the hypotheses can be weakened, but otherwise looks ready
+-- Upstreaming status: upstreamed (moved to Mathlib.Topology.Order.DenselyOrdered) in
+-- https://github.com/leanprover-community/mathlib4/pull/37550
 
 theorem nonempty_nhds_inter_Ioi {α : Type*} [LinearOrder α] [DenselyOrdered α]
     [TopologicalSpace α] [OrderTopology α]