diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean
index 60d13f85..cf7928cb 100644
--- a/Analysis/MeasureTheory/Section_1_4_3.lean
+++ b/Analysis/MeasureTheory/Section_1_4_3.lean
@@ -175,7 +175,8 @@ theorem FinitelyAdditiveMeasure.isCountablyAdditive_restrict_alg {X:Type*} {B B'
 def CountablyAdditiveMeasure.restrict_alg {X:Type*} {B B': ConcreteSigmaAlgebra X} (μ: CountablyAdditiveMeasure B) (hBB' : B' ≤ B) : CountablyAdditiveMeasure B' :=
   {
     toFinitelyAdditiveMeasure := μ.toFinitelyAdditiveMeasure.restrict_alg hBB',
-    measure_countable_additive := by sorry
+    measure_countable_additive := fun E hE hdisj =>
+      μ.measure_countable_additive E (fun n => hBB' (E n) (hE n)) hdisj
   }
 
 /-- Example 1.4.29 (Dirac measure) -/