diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean
deleted file mode 100644
index 9db98eb..0000000
--- a/Nevanlinna/complexHarmonic.examples.lean
+++ /dev/null
@@ -1,592 +0,0 @@
-import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
-import Nevanlinna.complexHarmonic
-import Nevanlinna.holomorphic
-
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
-variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁]
-variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
-
-
-theorem holomorphicAt_is_harmonicAt
-  {f : ℂ → F₁}
-  {z : ℂ}
-  (hf : HolomorphicAt f z) :
-  HarmonicAt f z := by
-
-  let t := {x | HolomorphicAt f x}
-  have ht : IsOpen t := HolomorphicAt_isOpen f
-  have hz : z ∈ t := by exact hf
-
-  constructor
-  · -- ContDiffAt ℝ 2 f z
-    exact HolomorphicAt_contDiffAt hf
-
-  · -- Δ f =ᶠ[nhds z] 0
-    apply Filter.eventuallyEq_iff_exists_mem.2
-    use t
-    constructor
-    · exact IsOpen.mem_nhds ht hz
-    · intro w hw
-      unfold Complex.laplace
-      simp
-      rw [partialDeriv_eventuallyEq ℝ (CauchyRiemann'₆ hw) Complex.I]
-      rw [partialDeriv_smul'₂]
-      simp
-
-      rw [partialDeriv_commAt (HolomorphicAt_contDiffAt hw) Complex.I 1]
-      rw [partialDeriv_eventuallyEq ℝ (CauchyRiemann'₆ hw) 1]
-      rw [partialDeriv_smul'₂]
-      simp
-
-      rw [← smul_assoc]
-      simp
-
-
-theorem re_of_holomorphicAt_is_harmonicAr
-  {f : ℂ → ℂ}
-  {z : ℂ}
-  (h : HolomorphicAt f z) :
-  HarmonicAt (Complex.reCLM ∘ f) z := by
-  apply harmonicAt_comp_CLM_is_harmonicAt
-  exact holomorphicAt_is_harmonicAt h
-
-
-theorem im_of_holomorphicAt_is_harmonicAt
-  {f : ℂ → ℂ}
-  {z : ℂ}
-  (h : HolomorphicAt f z) :
-  HarmonicAt (Complex.imCLM ∘ f) z := by
-  apply harmonicAt_comp_CLM_is_harmonicAt
-  exact holomorphicAt_is_harmonicAt h
-
-
-theorem antiholomorphicAt_is_harmonicAt
-  {f : ℂ → ℂ}
-  {z : ℂ}
-  (h : HolomorphicAt f z) :
-  HarmonicAt (Complex.conjCLE ∘ f) z := by
-  apply harmonicAt_iff_comp_CLE_is_harmonicAt.1
-  exact holomorphicAt_is_harmonicAt h
-
-
-theorem log_normSq_of_holomorphicAt_is_harmonicAt
-  {f : ℂ → ℂ}
-  {z : ℂ}
-  (h₁f : HolomorphicAt f z)
-  (h₂f : f z ≠ 0) :
-  HarmonicAt (Real.log ∘ Complex.normSq ∘ f) z := by
-
-  -- For later use
-  have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by
-    rw [Complex.mem_slitPlane_iff, Complex.mem_slitPlane_iff]
-    simp at hz
-    rw [Complex.ext_iff] at hz
-    push_neg at hz
-    simp at hz
-    simp
-    by_contra contra
-    push_neg at contra
-    exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2
-
-  -- First prove the theorem for functions with image in the slitPlane
-  have lem₁ : ∀ g : ℂ → ℂ, (HolomorphicAt g z) → (g z ≠ 0) → (g z ∈ Complex.slitPlane) → HarmonicAt (Real.log ∘ Complex.normSq ∘ g) z := by
-    intro g h₁g h₂g h₃g
-
-    -- Rewrite the log |g|² as Complex.log (g * gc)
-    suffices hyp : HarmonicAt (Complex.log ∘ ((Complex.conjCLE ∘ g) * g)) z from by
-      have : Real.log ∘ Complex.normSq ∘ g = Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g := by
-        funext x
-        simp
-      rw [this]
-
-      have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g = Complex.log ∘ ((Complex.conjCLE ∘ g) * g) := by
-        funext x
-        simp
-        rw [Complex.ofReal_log]
-        rw [Complex.normSq_eq_conj_mul_self]
-        exact Complex.normSq_nonneg (g x)
-      rw [← this] at hyp
-      apply harmonicAt_comp_CLM_is_harmonicAt hyp
-
-    -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
-    -- This uses the assumption that g z is in Complex.slitPlane
-    have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.log ∘ Complex.conjCLE ∘ g + Complex.log ∘ g) := by
-      apply Filter.eventuallyEq_iff_exists_mem.2
-      use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
-      constructor
-      · apply ContinuousAt.preimage_mem_nhds
-        · exact (HolomorphicAt_differentiableAt h₁g).continuousAt
-        · apply IsOpen.mem_nhds
-          apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
-          constructor
-          · exact h₃g
-          · exact h₂g
-      · intro x hx
-        simp
-        rw [Complex.log_mul_eq_add_log_iff _ hx.2]
-        rw [Complex.arg_conj]
-        simp [Complex.slitPlane_arg_ne_pi hx.1]
-        constructor
-        · exact Real.pi_pos
-        · exact Real.pi_nonneg
-        simp
-        apply hx.2
-
-    -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
-    -- This uses the assumption that g z is in Complex.slitPlane
-    have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.conjCLE ∘ Complex.log ∘ g + Complex.log ∘ g) := by
-      apply Filter.eventuallyEq_iff_exists_mem.2
-      use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
-      constructor
-      · apply ContinuousAt.preimage_mem_nhds
-        · exact (HolomorphicAt_differentiableAt h₁g).continuousAt
-        · apply IsOpen.mem_nhds
-          apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
-          constructor
-          · exact h₃g
-          · exact h₂g
-      · intro x hx
-        simp
-        rw [← Complex.log_conj]
-        rw [Complex.log_mul_eq_add_log_iff _ hx.2]
-        rw [Complex.arg_conj]
-        simp [Complex.slitPlane_arg_ne_pi hx.1]
-        constructor
-        · exact Real.pi_pos
-        · exact Real.pi_nonneg
-        simp
-        apply hx.2
-        apply Complex.slitPlane_arg_ne_pi hx.1
-
-    rw [HarmonicAt_eventuallyEq this]
-    apply harmonicAt_add_harmonicAt_is_harmonicAt
-    · rw [← harmonicAt_iff_comp_CLE_is_harmonicAt]
-      apply holomorphicAt_is_harmonicAt
-      apply HolomorphicAt_comp
-      use Complex.slitPlane
-      constructor
-      · apply IsOpen.mem_nhds
-        exact Complex.isOpen_slitPlane
-        assumption
-      · exact fun z a => Complex.differentiableAt_log a
-      exact h₁g
-    · apply holomorphicAt_is_harmonicAt
-      apply HolomorphicAt_comp
-      use Complex.slitPlane
-      constructor
-      · apply IsOpen.mem_nhds
-        exact Complex.isOpen_slitPlane
-        assumption
-      · exact fun z a => Complex.differentiableAt_log a
-      exact h₁g
-
-  by_cases h₃f : f z ∈ Complex.slitPlane
-  · exact lem₁ f h₁f h₂f h₃f
-  · have : Complex.normSq ∘ f = Complex.normSq ∘ (-f) := by funext; simp
-    rw [this]
-    apply lem₁ (-f)
-    · exact HolomorphicAt_neg h₁f
-    · simpa
-    · exact (slitPlaneLemma h₂f).resolve_left h₃f
-
-
-theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
-  Harmonic f := by
-
-  -- f is real C²
-  have f_is_real_C2 : ContDiff ℝ 2 f :=
-    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
-
-  have fI_is_real_differentiable : Differentiable ℝ (partialDeriv ℝ 1 f) := by
-    exact (partialDeriv_contDiff ℝ f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞)
-
-  constructor
-  · -- f is two times real continuously differentiable
-    exact f_is_real_C2
-
-  · -- Laplace of f is zero
-    unfold Complex.laplace
-    rw [CauchyRiemann₄ h]
-
-    -- This lemma says that partial derivatives commute with complex scalar
-    -- multiplication. This is a consequence of partialDeriv_compContLin once we
-    -- note that complex scalar multiplication is continuous ℝ-linear.
-    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → F₁, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
-      intro v s g hg
-
-      -- Present scalar multiplication as a continuous ℝ-linear map. This is
-      -- horrible, there must be better ways to do that.
-      let sMuls : F₁ →L[ℝ] F₁ :=
-      {
-        toFun := fun x ↦ s • x
-        map_add' := by exact fun x y => DistribSMul.smul_add s x y
-        map_smul' := by exact fun m x => (smul_comm ((RingHom.id ℝ) m) s x).symm
-        cont := continuous_const_smul s
-      }
-
-      -- Bring the goal into a form that is recognized by
-      -- partialDeriv_compContLin.
-      have : s • g = sMuls ∘ g := by rfl
-      rw [this]
-
-      rw [partialDeriv_compContLin ℝ hg]
-      rfl
-
-    rw [this]
-    rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
-    rw [CauchyRiemann₄ h]
-    rw [this]
-    rw [← smul_assoc]
-    simp
-
-    -- Subgoals coming from the application of 'this'
-    -- Differentiable ℝ (Real.partialDeriv 1 f)
-    exact fI_is_real_differentiable
-    -- Differentiable ℝ (Real.partialDeriv 1 f)
-    exact fI_is_real_differentiable
-
-
-theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpen s) (h : DifferentiableOn ℂ f s) :
-  HarmonicOn f s := by
-
-  -- f is real C²
-  have f_is_real_C2 : ContDiffOn ℝ 2 f s :=
-    ContDiffOn.restrict_scalars ℝ (DifferentiableOn.contDiffOn h hs)
-
-  constructor
-  · -- f is two times real continuously differentiable
-    exact f_is_real_C2
-
-  · -- Laplace of f is zero
-    unfold Complex.laplace
-    intro z hz
-    simp
-    have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
-      unfold Filter.EventuallyEq
-      unfold Filter.Eventually
-      simp
-      refine mem_nhds_iff.mpr ?_
-      use s
-      constructor
-      · intro x hx
-        simp
-        apply CauchyRiemann₅
-        apply DifferentiableOn.differentiableAt h
-        exact IsOpen.mem_nhds hs hx
-      · constructor
-        · exact hs
-        · exact hz
-    rw [partialDeriv_eventuallyEq ℝ this Complex.I]
-    rw [partialDeriv_smul'₂]
-
-    simp
-    rw [partialDeriv_commOn hs f_is_real_C2 Complex.I 1 z hz]
-
-    have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
-      unfold Filter.EventuallyEq
-      unfold Filter.Eventually
-      simp
-      refine mem_nhds_iff.mpr ?_
-      use s
-      constructor
-      · intro x hx
-        simp
-        apply CauchyRiemann₅
-        apply DifferentiableOn.differentiableAt h
-        exact IsOpen.mem_nhds hs hx
-      · constructor
-        · exact hs
-        · exact hz
-    rw [partialDeriv_eventuallyEq ℝ this 1]
-    rw [partialDeriv_smul'₂]
-    simp
-    rw [← smul_assoc]
-    simp
-
-
-theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
-  Harmonic (Complex.reCLM ∘ f) := by
-  apply harmonic_comp_CLM_is_harmonic
-  exact holomorphic_is_harmonic h
-
-
-theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
-  Harmonic (Complex.imCLM ∘ f) := by
-  apply harmonic_comp_CLM_is_harmonic
-  exact holomorphic_is_harmonic h
-
-
-theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
-  Harmonic (Complex.conjCLE ∘ f) := by
-  apply harmonic_iff_comp_CLE_is_harmonic.1
-  exact holomorphic_is_harmonic h
-
-
-theorem log_normSq_of_holomorphicOn_is_harmonicOn'
-  {f : ℂ → ℂ}
-  {s : Set ℂ}
-  (hs : IsOpen s)
-  (h₁ : DifferentiableOn ℂ f s)
-  (h₂ : ∀ z ∈ s, f z ≠ 0)
-  (h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) :
-  HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
-
-  suffices hyp : HarmonicOn (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s from
-    (harmonicOn_comp_CLM_is_harmonicOn hs hyp : HarmonicOn (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s)
-
-  suffices hyp : HarmonicOn (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) s from by
-    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by
-      funext z
-      simp
-      rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
-      rw [Complex.normSq_eq_conj_mul_self]
-    rw [this]
-    exact hyp
-
-
-  -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f)
-  -- THIS IS WHERE WE USE h₃
-  have : ∀ z ∈ s, (Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f)) z = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) z := by
-    intro z hz
-    unfold Function.comp
-    simp
-    rw [Complex.log_mul_eq_add_log_iff]
-
-    have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
-      rw [Complex.arg_conj]
-      have : ¬ Complex.arg (f z) = Real.pi := by
-        exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
-      simp
-      tauto
-    rw [this]
-    simp
-    constructor
-    · exact Real.pi_pos
-    · exact Real.pi_nonneg
-    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
-    exact h₂ z hz
-
-  rw [HarmonicOn_congr hs this]
-  simp
-
-  apply harmonicOn_add_harmonicOn_is_harmonicOn hs
-
-  have : (fun x => Complex.log ((starRingEnd ℂ) (f x))) = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) := by
-    rfl
-  rw [this]
-
-  -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s
-  have : ∀ z ∈ s, (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) z = (Complex.conjCLE ∘ Complex.log ∘ f) z := by
-    intro z hz
-    unfold Function.comp
-    rw [Complex.log_conj]
-    rfl
-    exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
-  rw [HarmonicOn_congr hs this]
-
-  rw [← harmonicOn_iff_comp_CLE_is_harmonicOn]
-
-  apply holomorphicOn_is_harmonicOn
-  exact hs
-
-  intro z hz
-  apply DifferentiableAt.differentiableWithinAt
-  apply DifferentiableAt.comp
-
-
-
-  exact Complex.differentiableAt_log (h₃ z hz)
-  apply DifferentiableOn.differentiableAt h₁ -- (h₁ z hz)
-  exact IsOpen.mem_nhds hs hz
-  exact hs
-
-  -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s
-  apply holomorphicOn_is_harmonicOn hs
-  exact DifferentiableOn.clog h₁ h₃
-
-
-theorem log_normSq_of_holomorphicOn_is_harmonicOn
-  {f : ℂ → ℂ}
-  {s : Set ℂ}
-  (hs : IsOpen s)
-  (h₁ : DifferentiableOn ℂ f s)
-  (h₂ : ∀ z ∈ s, f z ≠ 0) :
-  HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
-
-  have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by
-    rw [Complex.mem_slitPlane_iff]
-    rw [Complex.mem_slitPlane_iff]
-    simp at hz
-    rw [Complex.ext_iff] at hz
-    push_neg at hz
-    simp at hz
-    simp
-    by_contra contra
-    push_neg at contra
-    exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2
-
-  let s₁ : Set ℂ := { z | f z ∈ Complex.slitPlane} ∩ s
-
-  have hs₁ : IsOpen s₁ := by
-    let A := DifferentiableOn.continuousOn h₁
-    let B := continuousOn_iff'.1 A
-    obtain ⟨u, hu₁, hu₂⟩ := B Complex.slitPlane Complex.isOpen_slitPlane
-    have : u ∩ s = s₁ := by
-      rw [← hu₂]
-      tauto
-    rw [← this]
-    apply IsOpen.inter hu₁ hs
-
-  have harm₁ : HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s₁ := by
-    apply log_normSq_of_holomorphicOn_is_harmonicOn'
-    exact hs₁
-    apply DifferentiableOn.mono h₁ (Set.inter_subset_right {z | f z ∈ Complex.slitPlane} s)
-    -- ∀ 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
-    apply hz.1
-
-  let s₂ : Set ℂ := { z | -f z ∈ Complex.slitPlane} ∩ s
-
-  have h₁' : DifferentiableOn ℂ (-f) s := by
-    rw [← differentiableOn_neg_iff]
-    simp
-    exact h₁
-
-  have hs₂ : IsOpen s₂ := by
-    let A := DifferentiableOn.continuousOn h₁'
-    let B := continuousOn_iff'.1 A
-    obtain ⟨u, hu₁, hu₂⟩ := B Complex.slitPlane Complex.isOpen_slitPlane
-    have : u ∩ s = s₂ := by
-      rw [← hu₂]
-      tauto
-    rw [← this]
-    apply IsOpen.inter hu₁ hs
-
-  have harm₂ : HarmonicOn (Real.log ∘ Complex.normSq ∘ (-f)) s₂ := by
-    apply log_normSq_of_holomorphicOn_is_harmonicOn'
-    exact hs₂
-    apply DifferentiableOn.mono h₁' (Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s)
-    -- ∀ z ∈ s₁, f z ≠ 0
-    intro z hz
-    simp
-    exact h₂ z (Set.mem_of_mem_inter_right hz)
-    -- ∀ z ∈ s₁, f z ∈ Complex.slitPlane
-    intro z hz
-    apply hz.1
-
-  apply HarmonicOn_of_locally_HarmonicOn
-  intro z hz
-  by_cases hfz : f z ∈ Complex.slitPlane
-  · use s₁
-    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]
-        exact harm₁
-  · use s₂
-    constructor
-    · exact hs₂
-    · constructor
-      · constructor
-        · apply Or.resolve_left (slitPlaneLemma (h₂ z hz)) hfz
-        · exact hz
-      · 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
-  {f : ℂ → ℂ}
-  (h₁ : Differentiable ℂ f)
-  (h₂ : ∀ z, f z ≠ 0)
-  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
-  Harmonic (Real.log ∘ Complex.normSq ∘ f) := by
-
-  suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from
-    (harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f))
-
-  suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by
-    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by
-      funext z
-      simp
-      rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
-      rw [Complex.normSq_eq_conj_mul_self]
-    rw [this]
-    exact hyp
-
-
-  -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f)
-  -- THIS IS WHERE WE USE h₃
-  have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
-    unfold Function.comp
-    funext z
-    simp
-    rw [Complex.log_mul_eq_add_log_iff]
-
-    have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
-      rw [Complex.arg_conj]
-      have : ¬ Complex.arg (f z) = Real.pi := by
-        exact Complex.slitPlane_arg_ne_pi (h₃ z)
-      simp
-      tauto
-    rw [this]
-    simp
-    constructor
-    · exact Real.pi_pos
-    · exact Real.pi_nonneg
-    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
-    exact h₂ z
-  rw [this]
-
-  apply harmonic_add_harmonic_is_harmonic
-  have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
-    funext z
-    unfold Function.comp
-    rw [Complex.log_conj]
-    rfl
-    exact Complex.slitPlane_arg_ne_pi (h₃ z)
-  rw [this]
-  rw [← harmonic_iff_comp_CLE_is_harmonic]
-
-  repeat
-    apply holomorphic_is_harmonic
-    intro z
-    apply DifferentiableAt.comp
-    exact Complex.differentiableAt_log (h₃ z)
-    exact h₁ z
-
-
-theorem logabs_of_holomorphic_is_harmonic
-  {f : ℂ → ℂ}
-  (h₁ : Differentiable ℂ f)
-  (h₂ : ∀ z, f z ≠ 0)
-  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
-  Harmonic (fun z ↦ Real.log ‖f z‖) := by
-
-  -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
-  have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
-    funext z
-    simp
-    unfold Complex.abs
-    simp
-    rw [Real.log_sqrt]
-    rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
-    exact Complex.normSq_nonneg (f z)
-  rw [this]
-
-  -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
-  apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1
-
-  exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃
diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index cdd9e9c..d604f03 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -163,6 +163,20 @@ theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic
     simp
 
 
+theorem harmonicAt_smul_const_is_harmonicAt
+  {f : ℂ → F}
+  {x : ℂ}
+  {c : ℝ}
+  (h : HarmonicAt f x) :
+  HarmonicAt (c • f) x := by
+  constructor
+  · exact ContDiffAt.const_smul c h.1
+  · rw [laplace_smul]
+    have A := Filter.EventuallyEq.const_smul h.2 c
+    simp at A
+    assumption
+
+
 theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c ≠ 0) :
   Harmonic f ↔ Harmonic (c • f) := by
   constructor
@@ -171,6 +185,18 @@ theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c 
     exact fun a => harmonic_smul_const_is_harmonic a
 
 
+theorem harmonicAt_iff_smul_const_is_harmonicAt
+  {f : ℂ → F}
+  {x : ℂ}
+  {c : ℝ}
+  (hc : c ≠ 0) :
+  HarmonicAt f x ↔ HarmonicAt (c • f) x := by
+  constructor
+  · exact harmonicAt_smul_const_is_harmonicAt
+  · nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)]
+    exact fun a => harmonicAt_smul_const_is_harmonicAt a
+
+
 theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) :
   Harmonic (l ∘ f) := by
 
diff --git a/Nevanlinna/harmonicAt.examples.lean b/Nevanlinna/harmonicAt.examples.lean
new file mode 100644
index 0000000..0dff6b6
--- /dev/null
+++ b/Nevanlinna/harmonicAt.examples.lean
@@ -0,0 +1,211 @@
+import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+import Nevanlinna.complexHarmonic
+import Nevanlinna.holomorphicAt
+
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]
+
+
+theorem holomorphicAt_is_harmonicAt
+  {f : ℂ → F}
+  {z : ℂ}
+  (hf : HolomorphicAt f z) :
+  HarmonicAt f z := by
+
+  let t := {x | HolomorphicAt f x}
+  have ht : IsOpen t := HolomorphicAt_isOpen f
+  have hz : z ∈ t := by exact hf
+
+  constructor
+  · -- ContDiffAt ℝ 2 f z
+    exact hf.contDiffAt
+
+  · -- Δ f =ᶠ[nhds z] 0
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use t
+    constructor
+    · exact IsOpen.mem_nhds ht hz
+    · intro w hw
+      unfold Complex.laplace
+      simp
+      rw [partialDeriv_eventuallyEq ℝ hw.CauchyRiemannAt Complex.I]
+      rw [partialDeriv_smul'₂]
+      simp
+
+      rw [partialDeriv_commAt hw.contDiffAt Complex.I 1]
+      rw [partialDeriv_eventuallyEq ℝ hw.CauchyRiemannAt 1]
+      rw [partialDeriv_smul'₂]
+      simp
+
+      rw [← smul_assoc]
+      simp
+
+
+theorem re_of_holomorphicAt_is_harmonicAr
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h : HolomorphicAt f z) :
+  HarmonicAt (Complex.reCLM ∘ f) z := by
+  apply harmonicAt_comp_CLM_is_harmonicAt
+  exact holomorphicAt_is_harmonicAt h
+
+
+theorem im_of_holomorphicAt_is_harmonicAt
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h : HolomorphicAt f z) :
+  HarmonicAt (Complex.imCLM ∘ f) z := by
+  apply harmonicAt_comp_CLM_is_harmonicAt
+  exact holomorphicAt_is_harmonicAt h
+
+
+theorem antiholomorphicAt_is_harmonicAt
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h : HolomorphicAt f z) :
+  HarmonicAt (Complex.conjCLE ∘ f) z := by
+  apply harmonicAt_iff_comp_CLE_is_harmonicAt.1
+  exact holomorphicAt_is_harmonicAt h
+
+
+theorem log_normSq_of_holomorphicAt_is_harmonicAt
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h₁f : HolomorphicAt f z)
+  (h₂f : f z ≠ 0) :
+  HarmonicAt (Real.log ∘ Complex.normSq ∘ f) z := by
+
+  -- For later use
+  have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by
+    rw [Complex.mem_slitPlane_iff, Complex.mem_slitPlane_iff]
+    simp at hz
+    rw [Complex.ext_iff] at hz
+    push_neg at hz
+    simp at hz
+    simp
+    by_contra contra
+    push_neg at contra
+    exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2
+
+  -- First prove the theorem for functions with image in the slitPlane
+  have lem₁ : ∀ g : ℂ → ℂ, (HolomorphicAt g z) → (g z ≠ 0) → (g z ∈ Complex.slitPlane) → HarmonicAt (Real.log ∘ Complex.normSq ∘ g) z := by
+    intro g h₁g h₂g h₃g
+
+    -- Rewrite the log |g|² as Complex.log (g * gc)
+    suffices hyp : HarmonicAt (Complex.log ∘ ((Complex.conjCLE ∘ g) * g)) z from by
+      have : Real.log ∘ Complex.normSq ∘ g = Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g := by
+        funext x
+        simp
+      rw [this]
+
+      have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g = Complex.log ∘ ((Complex.conjCLE ∘ g) * g) := by
+        funext x
+        simp
+        rw [Complex.ofReal_log]
+        rw [Complex.normSq_eq_conj_mul_self]
+        exact Complex.normSq_nonneg (g x)
+      rw [← this] at hyp
+      apply harmonicAt_comp_CLM_is_harmonicAt hyp
+
+    -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
+    -- This uses the assumption that g z is in Complex.slitPlane
+    have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.log ∘ Complex.conjCLE ∘ g + Complex.log ∘ g) := by
+      apply Filter.eventuallyEq_iff_exists_mem.2
+      use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
+      constructor
+      · apply ContinuousAt.preimage_mem_nhds
+        · exact h₁g.differentiableAt.continuousAt
+        · apply IsOpen.mem_nhds
+          apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
+          constructor
+          · exact h₃g
+          · exact h₂g
+      · intro x hx
+        simp
+        rw [Complex.log_mul_eq_add_log_iff _ hx.2]
+        rw [Complex.arg_conj]
+        simp [Complex.slitPlane_arg_ne_pi hx.1]
+        constructor
+        · exact Real.pi_pos
+        · exact Real.pi_nonneg
+        simp
+        apply hx.2
+
+    -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc
+    -- This uses the assumption that g z is in Complex.slitPlane
+    have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.conjCLE ∘ Complex.log ∘ g + Complex.log ∘ g) := by
+      apply Filter.eventuallyEq_iff_exists_mem.2
+      use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ)
+      constructor
+      · apply ContinuousAt.preimage_mem_nhds
+        · exact h₁g.differentiableAt.continuousAt
+        · apply IsOpen.mem_nhds
+          apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne
+          constructor
+          · exact h₃g
+          · exact h₂g
+      · intro x hx
+        simp
+        rw [← Complex.log_conj]
+        rw [Complex.log_mul_eq_add_log_iff _ hx.2]
+        rw [Complex.arg_conj]
+        simp [Complex.slitPlane_arg_ne_pi hx.1]
+        constructor
+        · exact Real.pi_pos
+        · exact Real.pi_nonneg
+        simp
+        apply hx.2
+        apply Complex.slitPlane_arg_ne_pi hx.1
+
+    rw [HarmonicAt_eventuallyEq this]
+    apply harmonicAt_add_harmonicAt_is_harmonicAt
+    · rw [← harmonicAt_iff_comp_CLE_is_harmonicAt]
+      apply holomorphicAt_is_harmonicAt
+      apply HolomorphicAt_comp
+      use Complex.slitPlane
+      constructor
+      · apply IsOpen.mem_nhds
+        exact Complex.isOpen_slitPlane
+        assumption
+      · exact fun z a => Complex.differentiableAt_log a
+      exact h₁g
+    · apply holomorphicAt_is_harmonicAt
+      apply HolomorphicAt_comp
+      use Complex.slitPlane
+      constructor
+      · apply IsOpen.mem_nhds
+        exact Complex.isOpen_slitPlane
+        assumption
+      · exact fun z a => Complex.differentiableAt_log a
+      exact h₁g
+
+  by_cases h₃f : f z ∈ Complex.slitPlane
+  · exact lem₁ f h₁f h₂f h₃f
+  · have : Complex.normSq ∘ f = Complex.normSq ∘ (-f) := by funext; simp
+    rw [this]
+    apply lem₁ (-f)
+    · exact HolomorphicAt_neg h₁f
+    · simpa
+    · exact (slitPlaneLemma h₂f).resolve_left h₃f
+
+
+theorem logabs_of_holomorphicAt_is_harmonic
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h₁f : HolomorphicAt f z)
+  (h₂f : f z ≠ 0) :
+  HarmonicAt (fun w ↦ Real.log ‖f w‖) z := by
+
+  -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
+  have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
+    funext z
+    simp
+    unfold Complex.abs
+    simp
+    rw [Real.log_sqrt]
+    rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
+    exact Complex.normSq_nonneg (f z)
+  rw [this]
+
+  -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
+  apply (harmonicAt_iff_smul_const_is_harmonicAt (inv_ne_zero two_ne_zero)).1
+  exact log_normSq_of_holomorphicAt_is_harmonicAt h₁f h₂f
diff --git a/Nevanlinna/holomorphicAt.lean b/Nevanlinna/holomorphicAt.lean
new file mode 100644
index 0000000..e6ae80a
--- /dev/null
+++ b/Nevanlinna/holomorphicAt.lean
@@ -0,0 +1,159 @@
+import Mathlib.Analysis.Complex.TaylorSeries
+import Nevanlinna.cauchyRiemann
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G]
+
+def HolomorphicAt (f : E → F) (x : E) : Prop :=
+  ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z
+
+
+theorem HolomorphicAt_iff
+  {f : E → F}
+  {x : E} :
+  HolomorphicAt f x ↔ ∃ s :
+  Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, DifferentiableAt ℂ f z) := by
+  constructor
+  · intro hf
+    obtain ⟨t, h₁t, h₂t⟩ := hf
+    obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁t
+    use s
+    constructor
+    · assumption
+    · constructor
+      · assumption
+      · intro z hz
+        exact h₂t z (h₁s hz)
+  · intro hyp
+    obtain ⟨s, h₁s, h₂s, hf⟩ := hyp
+    use s
+    constructor
+    · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
+    · assumption
+
+
+theorem HolomorphicAt_isOpen
+  (f : E → F) :
+  IsOpen { x : E | HolomorphicAt f x } := by
+
+  rw [← subset_interior_iff_isOpen]
+  intro x hx
+  simp at hx
+  obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hx
+  use s
+  constructor
+  · simp
+    constructor
+    · exact h₁s
+    · intro x hx
+      simp
+      use s
+      constructor
+      · exact IsOpen.mem_nhds h₁s hx
+      · exact h₃s
+  · exact h₂s
+
+
+theorem HolomorphicAt_comp
+  {g : E → F}
+  {f : F → G}
+  {z : E}
+  (hf : HolomorphicAt f (g z))
+  (hg : HolomorphicAt g z) :
+  HolomorphicAt (f ∘ g) z := by
+  obtain ⟨UE, h₁UE, h₂UE⟩ := hg
+  obtain ⟨UF, h₁UF, h₂UF⟩ := hf
+  use UE ∩ g⁻¹' UF
+  constructor
+  · simp
+    constructor
+    · assumption
+    · apply ContinuousAt.preimage_mem_nhds
+      apply (h₂UE z (mem_of_mem_nhds h₁UE)).continuousAt
+      assumption
+  · intro x hx
+    apply DifferentiableAt.comp
+    apply h₂UF
+    exact hx.2
+    apply h₂UE
+    exact hx.1
+
+
+theorem HolomorphicAt_neg
+  {f : E → F}
+  {z : E}
+  (hf : HolomorphicAt f z) :
+  HolomorphicAt (-f) z := by
+  obtain ⟨UF, h₁UF, h₂UF⟩ := hf
+  use UF
+  constructor
+  · assumption
+  · intro z hz
+    apply differentiableAt_neg_iff.mp
+    simp
+    exact h₂UF z hz
+
+
+theorem HolomorphicAt.contDiffAt
+  [CompleteSpace F]
+  {f : ℂ → F}
+  {z : ℂ}
+  {n : ℕ}
+  (hf : HolomorphicAt f z) :
+  ContDiffAt ℝ n f z := by
+
+  let t := {x | HolomorphicAt f x}
+  have ht : IsOpen t := HolomorphicAt_isOpen f
+  have hz : z ∈ t := by exact hf
+
+  -- ContDiffAt ℝ _ f z
+  apply ContDiffOn.contDiffAt _ ((IsOpen.mem_nhds_iff ht).2 hz)
+  suffices h : ContDiffOn ℂ n f t from by
+    apply ContDiffOn.restrict_scalars ℝ h
+  apply DifferentiableOn.contDiffOn _ ht
+  intro w hw
+  apply DifferentiableAt.differentiableWithinAt
+  -- DifferentiableAt ℂ f w
+  let hfw : HolomorphicAt f w := hw
+  obtain ⟨s, _, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hfw
+  exact h₃s w h₂s
+
+
+theorem HolomorphicAt.differentiableAt
+  {f : ℂ → F}
+  {z : ℂ}
+  (hf : HolomorphicAt f z) :
+  DifferentiableAt ℂ f z := by
+  obtain ⟨s, _, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf
+  exact h₃s z h₂s
+
+
+theorem HolomorphicAt.CauchyRiemannAt
+  {f : ℂ → F}
+  {z : ℂ}
+  (h : HolomorphicAt f z) :
+  partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
+
+  obtain ⟨s, h₁s, hz, h₂f⟩ := HolomorphicAt_iff.1 h
+
+  apply Filter.eventuallyEq_iff_exists_mem.2
+  use s
+  constructor
+  · exact IsOpen.mem_nhds h₁s hz
+  · intro w hw
+    let h := h₂f w hw
+    -- WARNING This should go to partialDeriv
+    unfold partialDeriv
+    simp
+    conv =>
+      left
+      rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
+      simp
+      rw [← mul_one Complex.I]
+      rw [← smul_eq_mul]
+      rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1]
+    conv =>
+      right
+      right
+      rw [DifferentiableAt.fderiv_restrictScalars ℝ h]