From 4d3332b15d92456f0c64922b691722e08b82f1d8 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 3 Jun 2024 18:53:55 +0200
Subject: [PATCH] Update complexHarmonic.examples.lean

---
 Nevanlinna/complexHarmonic.examples.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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