diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean
index 60d13f85..edf88267 100644
--- a/Analysis/MeasureTheory/Section_1_4_3.lean
+++ b/Analysis/MeasureTheory/Section_1_4_3.lean
@@ -197,7 +197,7 @@ noncomputable instance CountablyAdditiveMeasure.instZero {X:Type*} (B: ConcreteS
   {
     zero := {
       toFinitelyAdditiveMeasure := 0
-      measure_countable_additive := by sorry
+      measure_countable_additive := fun _ _ _ => tsum_zero.symm
     }
   }