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

---
 Nevanlinna/complexHarmonic.examples.lean | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean
index 177810d..7f3ec14 100644
--- a/Nevanlinna/complexHarmonic.examples.lean
+++ b/Nevanlinna/complexHarmonic.examples.lean
@@ -246,8 +246,7 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
   {s : Set ℂ}
   (hs : IsOpen s)
   (h₁ : DifferentiableOn ℂ f s)
-  (h₂ : ∀ z ∈ s, f z ≠ 0)
-  (h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) :
+  (h₂ : ∀ z ∈ s, f z ≠ 0) :
   HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
 
   let s₁ : Set ℂ := { z | f z ∈ Complex.slitPlane} ∩ s
@@ -269,7 +268,8 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
     -- ∀ z ∈ s₁, f z ≠ 0
     exact fun z hz ↦ h₂ z (Set.mem_of_mem_inter_right hz)
     -- ∀ z ∈ s₁, f z ∈ Complex.slitPlane
-    exact fun z hz ↦ h₃ z (Set.mem_of_mem_inter_right hz)
+    intro z hz
+    apply hz.1
 
   let s₂ : Set ℂ := { z | -f z ∈ Complex.slitPlane} ∩ s
 
@@ -314,7 +314,19 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
         rw [← this]
         exact harm₁
   · use s₂
-    sorry
+    constructor
+    · exact hs₂
+    · constructor
+      · tauto
+      · have : s₂ = s ∩ s₂ := by
+          apply Set.right_eq_inter.mpr
+          exact Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s
+        rw [← this]
+        have : Real.log ∘ ⇑Complex.normSq ∘ f = Real.log ∘ ⇑Complex.normSq ∘ (-f) := by
+          funext x
+          simp
+        rw [this]
+        exact harm₂
 
 
 theorem log_normSq_of_holomorphic_is_harmonic