diff --git a/OpenGALib/GeometricMeasureTheory/Varifold.lean b/OpenGALib/GeometricMeasureTheory/Varifold.lean
index ebc8e2e..7b0aba9 100644
--- a/OpenGALib/GeometricMeasureTheory/Varifold.lean
+++ b/OpenGALib/GeometricMeasureTheory/Varifold.lean
@@ -123,6 +123,11 @@ omit [MeasureTheory.MeasureSpace M] in
 theorem massOn_nonneg (V : Varifold M) (U : Set M) : 0 ≤ massOn V U :=
   ENNReal.toReal_nonneg
 
+omit [MeasureTheory.MeasureSpace M] in
+/-- Localized mass on the empty set is zero. -/
+@[simp] theorem massOn_empty (V : Varifold M) : massOn V ∅ = 0 := by
+  simp [massOn]
+
 omit [MeasureTheory.MeasureSpace M] in
 /-- Localized mass is monotone in the set. -/
 theorem massOn_mono (V : Varifold M) {U W : Set M} (h : U ⊆ W) :
@@ -133,6 +138,7 @@ theorem massOn_mono (V : Varifold M) {U W : Set M} (h : U ⊆ W) :
 
 omit [MeasureTheory.MeasureSpace M] in
 /-- The total mass equals the localized mass on the whole space. -/
+@[simp]
 theorem massOn_univ (V : Varifold M) : massOn V Set.univ = mass V := rfl
 
 /-- $p \in \mathrm{spt}\|V\|$ iff every open ball around $p$ has positive