diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean
index 60d13f85..de895913 100644
--- a/Analysis/MeasureTheory/Section_1_4_3.lean
+++ b/Analysis/MeasureTheory/Section_1_4_3.lean
@@ -85,9 +85,11 @@ noncomputable instance FinitelyAdditiveMeasure.instSmul {X:Type*} {B: ConcreteBo
     smul := fun c μ =>
         {
         measure := fun A => c * μ.measure A
-        measure_pos := by sorry
-        measure_empty := by sorry
-        measure_finite_additive := by sorry
+        measure_pos := fun A hA => mul_nonneg (zero_le _) (μ.measure_pos A hA)
+        measure_empty := by simp [μ.measure_empty]
+        measure_finite_additive := fun E F hE hF hdisj => by
+          simp [μ.measure_finite_additive E F hE hF hdisj]
+          exact mul_add (c : EReal) _ _
         }
 }