diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean
index 7f3ec14..a3d241e 100644
--- a/Nevanlinna/complexHarmonic.examples.lean
+++ b/Nevanlinna/complexHarmonic.examples.lean
@@ -317,7 +317,11 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
     constructor
     · exact hs₂
     · constructor
-      · tauto
+      · constructor
+        · simp
+          rw [Complex.mem_slitPlane_iff]
+          rw [Complex.mem_slitPlane_iff] at hfz
+          simp at hfz
       · have : s₂ = s ∩ s₂ := by
           apply Set.right_eq_inter.mpr
           exact Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s