diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean
index 60d13f85..e73a142a 100644
--- a/Analysis/MeasureTheory/Section_1_4_3.lean
+++ b/Analysis/MeasureTheory/Section_1_4_3.lean
@@ -231,10 +231,29 @@ noncomputable instance CountablyAdditiveMeasure.instSmul {X:Type*} {B: ConcreteS
 
 noncomputable instance CountablyAdditiveMeasure.instDistribMulAction {X:Type*} {B: ConcreteSigmaAlgebra X} : DistribMulAction ENNReal (CountablyAdditiveMeasure B) :=
 {
-  smul_zero := by sorry,
-  smul_add := by sorry,
-  one_smul := by sorry,
-  mul_smul := by sorry
+  smul_zero := by
+    intro c
+    congr 1
+    ext A
+    simp
+  smul_add := by
+    intro c μ ν
+    cases μ; cases ν
+    congr 1
+    ext A
+    exact left_distrib (c : EReal) _ _
+  one_smul := by
+    intro μ
+    cases μ
+    congr 1
+    ext A
+    exact one_smul EReal _
+  mul_smul := by
+    intro a b μ
+    cases μ
+    congr 1
+    ext A
+    exact mul_assoc (a : EReal) _ _
 }
 
 /-- Exercise 1.4.22(ii) -/