diff --git a/Nevanlinna/specialFunctions_Integral_log_sin.lean b/Nevanlinna/specialFunctions_Integral_log_sin.lean
index 1a968e6..4af841d 100644
--- a/Nevanlinna/specialFunctions_Integral_log_sin.lean
+++ b/Nevanlinna/specialFunctions_Integral_log_sin.lean
@@ -105,6 +105,8 @@ lemma intervalIntegrable_log_sin₁ : IntervalIntegrable (log ∘ sin) volume 0
 
   have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by
     apply IntervalIntegrable.norm
+    -- Extract lemma here: log is integrable on [0, 1], and in fact on any
+    -- interval [a, b]
     rw [← neg_neg log]
     apply IntervalIntegrable.neg
     apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))