diff --git a/.DS_Store b/.DS_Store
deleted file mode 100644
index 23f4574..0000000
Binary files a/.DS_Store and /dev/null differ
diff --git a/.gitignore b/.gitignore
index d701102..acf3987 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 /build
 /lake-packages/*
 .lake/packages/*
-.lake/build
\ No newline at end of file
+.lake/build
+.DS_Store
diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
index a3432b5..18125cb 100644
--- a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
@@ -80,26 +80,26 @@ lemma left_zero : potential 0 Φ2 m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵
 
 ## Potential bounded from below
 
-TODO: Complete this section.
-
 -/
 
+/-! TODO: Prove bounded properties of the 2HDM potential. -/
+
 /-!
 
 ## Smoothness of the potential
 
-TODO: Complete this section.
-
 -/
 
+/-! TODO: Prove smoothness properties of the 2HDM potential. -/
+
 /-!
 
 ## Invariance of the potential under gauge transformations
 
-TODO: Complete this section.
-
 -/
 
+/-! TODO: Prove invariance properties of the 2HDM potential. -/
+
 end potential
 
 end