From 60f598b13c189132f6ebbabf4f828930a5289aa8 Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Mon, 7 Sep 2026 16:27:25 +0530
Subject: [PATCH] Fill the additive commutative monoid instance for finitely
 additive measures.

Addition is pointwise on EReal-valued set functions, so the monoid laws follow from those of EReal.
---
 Analysis/MeasureTheory/Section_1_4_3.lean | 28 +++++++++++++++++++----
 1 file changed, 24 insertions(+), 4 deletions(-)

diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean
index 60d13f856..ccac0f755 100644
--- a/Analysis/MeasureTheory/Section_1_4_3.lean
+++ b/Analysis/MeasureTheory/Section_1_4_3.lean
@@ -93,10 +93,30 @@ noncomputable instance FinitelyAdditiveMeasure.instSmul {X:Type*} {B: ConcreteBo
 
 noncomputable instance FinitelyAdditiveMeasure.instAddCommMonoid {X:Type*} {B: ConcreteBooleanAlgebra X} : AddCommMonoid (FinitelyAdditiveMeasure B) :=
 {
-  add_assoc := by sorry,
-  zero_add := by sorry,
-  add_zero := by sorry,
-  add_comm := by sorry
+  add_assoc := by
+    intro μ ν ρ
+    cases μ; cases ν; cases ρ
+    congr 1
+    ext A
+    exact add_assoc _ _ _
+  zero_add := by
+    intro μ
+    cases μ
+    congr 1
+    ext A
+    exact zero_add _
+  add_zero := by
+    intro μ
+    cases μ
+    congr 1
+    ext A
+    exact add_zero _
+  add_comm := by
+    intro μ ν
+    cases μ; cases ν
+    congr 1
+    ext A
+    exact add_comm _ _
   nsmul := nsmulRec
 }