diff --git a/Mathlib/MeasureTheory/Function/EssSup.lean b/Mathlib/MeasureTheory/Function/EssSup.lean
index 503c49f68e8df..db6581f557a6c 100644
--- a/Mathlib/MeasureTheory/Function/EssSup.lean
+++ b/Mathlib/MeasureTheory/Function/EssSup.lean
@@ -6,6 +6,7 @@ Authors: Rémy Degenne
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
 import Mathlib.MeasureTheory.Measure.Count
 import Mathlib.Order.Filter.ENNReal
+import Mathlib.Probability.ConditionalProbability
 
 /-!
 # Essential supremum and infimum
@@ -28,9 +29,8 @@ sense). We do not define that quantity here, which is simply the supremum of a m
 -/
 
 
-open MeasureTheory Filter Set TopologicalSpace
-
-open ENNReal MeasureTheory NNReal
+open Filter MeasureTheory ProbabilityTheory Set TopologicalSpace
+open scoped ENNReal NNReal
 
 variable {α β : Type*} {m : MeasurableSpace α} {μ ν : Measure α}
 
@@ -94,6 +94,12 @@ variable [MeasurableSingletonClass α]
 @[simp] lemma essInf_count_eq_ciInf (hf : BddBelow (Set.range f)) :
     essInf f .count = ⨅ a, f a := essInf_eq_ciInf (by simp) hf
 
+@[simp] lemma essSup_cond_count_eq_ciSup [Finite α] (hf : BddAbove (Set.range f)) :
+    essSup f .count[|.univ] = ⨆ a, f a := essSup_eq_ciSup (by simp [cond_apply, Set.finite_univ]) hf
+
+@[simp] lemma essInf_cond_count_eq_ciInf [Finite α] (hf : BddBelow (Set.range f)) :
+    essInf f .count[|.univ] = ⨅ a, f a := essInf_eq_ciInf (by simp [cond_apply, Set.finite_univ]) hf
+
 end ConditionallyCompleteLattice
 
 section ConditionallyCompleteLinearOrder