Update complexHarmonic.examples.lean

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,23 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
         rw [← this]
         exact harm₁
   · use s₂
-    sorry
+    constructor
+    · exact hs₂
+    · constructor
+      · 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
+        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