diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean
index 60d13f85..ce017c68 100644
--- a/Analysis/MeasureTheory/Section_1_4_3.lean
+++ b/Analysis/MeasureTheory/Section_1_4_3.lean
@@ -121,8 +121,8 @@ def FinitelyAdditiveMeasure.restrict {X:Type*} {B: ConcreteBooleanAlgebra X} (μ
 noncomputable def FinitelyAdditiveMeasure.counting (X:Type*) : FinitelyAdditiveMeasure (⊤  : ConcreteBooleanAlgebra X) :=
   {
     measure := fun E => ENat.card E
-    measure_pos := by sorry
-    measure_empty := by sorry
+    measure_pos := fun _ _ => by positivity
+    measure_empty := by simp
     measure_finite_additive := by sorry
   }