Nevanlinna/complexHarmonic.examples.lean

@@ -246,7 +246,8 @@ 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 ≠ 0)
+  (h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) :
   HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
 
   let s₁ : Set ℂ := { z | f z ∈ Complex.slitPlane} ∩ s
@@ -268,8 +269,7 @@ 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
-    intro z hz
+    exact fun z hz ↦ h₃ z (Set.mem_of_mem_inter_right hz)
-    apply hz.1
 
   let s₂ : Set ℂ := { z | -f z ∈ Complex.slitPlane} ∩ s
 
@@ -314,23 +314,7 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
         rw [← this]
         exact harm₁
   · use s₂
-    constructor
+    sorry
-    · 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