23 changed files with 87 additions and 1290 deletions
--- a/Nevanlinna/analyticAt.lean
+++ b/Nevanlinna/analyticAt.lean
@ -2,20 +2,6 @@ import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Analytic.Linear

-open Topology
-
-
-theorem AnalyticAt.order_neq_top_iff
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticAt ℂ f z₀) :
-  hf.order ≠ ⊤ ↔ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (hf.order.toNat) • g z := by
-  rw [← hf.order_eq_nat_iff]
-  constructor
-  · intro h₁f
-    exact Eq.symm (ENat.coe_toNat h₁f)
-  · intro h₁f
-    exact ENat.coe_toNat_eq_self.mp (id (Eq.symm h₁f))


 theorem AnalyticAt.order_mul
@ -119,6 +105,10 @@ theorem AnalyticAt.supp_order_toNat
  simp [hf.order_eq_zero_iff.2 h₁f]


+theorem ContinuousLinearEquiv.analyticAt
+  (ℓ : ℂ ≃L[ℂ] ℂ) (z₀ : ℂ) : AnalyticAt ℂ (⇑ℓ) z₀ := ℓ.toContinuousLinearMap.analyticAt z₀
+
+
 theorem eventually_nhds_comp_composition
  {f₁ f₂ ℓ : ℂ → ℂ}
  {z₀ : ℂ}
@ -234,77 +224,3 @@ theorem AnalyticAt.order_comp_CLE
    rw [this]

    simp
-
-
-theorem AnalyticAt.localIdentity
-  {f g : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticAt ℂ f z₀)
-  (hg : AnalyticAt ℂ g z₀) :
-  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
-  intro h
-  let Δ := f - g
-  have : AnalyticAt ℂ Δ z₀ := AnalyticAt.sub hf hg
-  have t₁ : Δ =ᶠ[𝓝[≠] z₀] 0 := by
-    exact Filter.eventuallyEq_iff_sub.mp h
-
-  have : Δ =ᶠ[𝓝 z₀] 0 := by
-    rcases (AnalyticAt.eventually_eq_zero_or_eventually_ne_zero this) with h | h
-    · exact h
-    · have := Filter.EventuallyEq.eventually t₁
-      let A := Filter.eventually_and.2 ⟨this, h⟩
-      let _ := Filter.Eventually.exists A
-      tauto
-  exact Filter.eventuallyEq_iff_sub.mpr this
-
-
-theorem AnalyticAt.mul₁
-  {f g : ℂ → ℂ}
-  {z : ℂ}
-  (hf : AnalyticAt ℂ f z)
-  (hg : AnalyticAt ℂ g z) :
-  AnalyticAt ℂ (f * g) z := by
-  rw [(by rfl : f * g = (fun x ↦ f x * g x))]
-  exact mul hf hg
-
-
-theorem analyticAt_finprod
-  {α : Type}
-  {f : α → ℂ → ℂ}
-  {z : ℂ}
-  (hf : ∀ a, AnalyticAt ℂ (f a) z) :
-  AnalyticAt ℂ (∏ᶠ a, f a) z := by
-  by_cases h₁f : (Function.mulSupport f).Finite
-  · rw [finprod_eq_prod f h₁f]
-    rw [Finset.prod_fn h₁f.toFinset f]
-    exact Finset.analyticAt_prod h₁f.toFinset (fun a _ ↦ hf a)
-  · rw [finprod_of_infinite_mulSupport h₁f]
-    exact analyticAt_const
-
-
-lemma AnalyticAt.zpow_nonneg
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  {n : ℤ}
-  (hf : AnalyticAt ℂ f z₀)
-  (hn : 0 ≤ n) :
-  AnalyticAt ℂ (fun x ↦ (f x) ^ n) z₀ := by
-  simp_rw [(Eq.symm (Int.toNat_of_nonneg hn) : n = OfNat.ofNat n.toNat), zpow_ofNat]
-  apply AnalyticAt.pow hf
-
-
-theorem AnalyticAt.zpow
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  {n : ℤ}
-  (h₁f : AnalyticAt ℂ f z₀)
-  (h₂f : f z₀ ≠ 0) :
-  AnalyticAt ℂ (fun x ↦ (f x) ^ n) z₀ := by
-  by_cases hn : 0 ≤ n
-  · exact zpow_nonneg h₁f hn
-  · rw [(Int.eq_neg_comm.mp rfl : n = - (- n))]
-    conv =>
-      arg 2
-      intro x
-      rw [zpow_neg]
-    exact AnalyticAt.inv (zpow_nonneg h₁f (by linarith)) (zpow_ne_zero (-n) h₂f)
--- a/Nevanlinna/analyticOnNhd_divisor.lean
+++ b/Nevanlinna/analyticOnNhd_divisor.lean
@ -1,59 +0,0 @@
-import Nevanlinna.analyticAt
-import Nevanlinna.divisor
-
-open scoped Interval Topology
-open Real Filter MeasureTheory intervalIntegral
-
-
-noncomputable def AnalyticOnNhd.zeroDivisor
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOnNhd ℂ f U) :
-  Divisor U where
-
-  toFun := by
-    intro z
-    if hz : z ∈ U then
-      exact ((hf z hz).order.toNat : ℤ)
-    else
-      exact 0
-
-  supportInU := by
-    intro z hz
-    simp at hz
-    by_contra h₂z
-    simp [h₂z] at hz
-
-  locallyFiniteInU := by
-    intro z hz
-
-    apply eventually_nhdsWithin_iff.2
-    rw [eventually_nhds_iff]
-
-    rcases AnalyticAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h
-    · rw [eventually_nhds_iff] at h
-      obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
-      use N
-      constructor
-      · intro y h₁y _
-        by_cases h₃y : y ∈ U
-        · simp [h₃y]
-          right
-          rw [AnalyticAt.order_eq_top_iff (hf y h₃y)]
-          rw [eventually_nhds_iff]
-          use N
-        · simp [h₃y]
-      · tauto
-
-    · rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h
-      obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
-      use N
-      constructor
-      · intro y h₁y h₂y
-        by_cases h₃y : y ∈ U
-        · simp [h₃y]
-          left
-          rw [AnalyticAt.order_eq_zero_iff (hf y h₃y)]
-          exact h₁N y h₁y h₂y
-        · simp [h₃y]
-      · tauto
--- a/Nevanlinna/analyticOnNhd_zeroSet.lean
+++ b/Nevanlinna/analyticOnNhd_zeroSet.lean
@ -4,17 +4,17 @@ import Mathlib.Analysis.Complex.Basic
 import Nevanlinna.analyticAt


-noncomputable def AnalyticOnNhd.order
-  {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOnNhd ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
+noncomputable def AnalyticOn.order
+  {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOn ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order


-theorem AnalyticOnNhd.order_eq_nat_iff
+theorem AnalyticOn.order_eq_nat_iff
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {z₀ : U}
-  (hf : AnalyticOnNhd ℂ f U)
+  (hf : AnalyticOn ℂ f U)
  (n : ℕ) :
-  hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
+  hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by

  constructor
  -- Direction →
@ -91,31 +91,31 @@ theorem AnalyticOnNhd.order_eq_nat_iff
  -- direction ←
  intro h
  obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
-  dsimp [AnalyticOnNhd.order]
+  dsimp [AnalyticOn.order]
  rw [AnalyticAt.order_eq_nat_iff]
  use g
  exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩


-theorem AnalyticOnNhd.support_of_order₁
+theorem AnalyticOn.support_of_order₁
  {f : ℂ → ℂ}
  {U : Set ℂ}
-  (hf : AnalyticOnNhd ℂ f U) :
+  (hf : AnalyticOn ℂ f U) :
  Function.support hf.order = U.restrict f⁻¹' {0} := by
  ext u
-  simp [AnalyticOnNhd.order]
+  simp [AnalyticOn.order]
  rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]


-theorem AnalyticOnNhd.eliminateZeros
+theorem AnalyticOn.eliminateZeros
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {A : Finset U}
-  (hf : AnalyticOnNhd ℂ f U)
+  (hf : AnalyticOn ℂ f U)
  (n : U → ℕ) :
-  (∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
+  (∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by

-  apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)
+  apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)

  -- case empty
  simp
@ -146,7 +146,7 @@ theorem AnalyticOnNhd.eliminateZeros
      intro b _
      apply AnalyticAt.pow
      apply AnalyticAt.sub
-      apply analyticAt_id
+      apply analyticAt_id ℂ
      exact analyticAt_const

    have h₂φ : h₁φ.order = (0 : ℕ) := by
@ -173,7 +173,7 @@ theorem AnalyticOnNhd.eliminateZeros
    rw [h₂φ]
    simp

-  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOnNhd.order_eq_nat_iff h₁g₀ (n b₀)).1 this
+  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this

  use g₁
  constructor
@ -203,7 +203,7 @@ theorem XX
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hU : IsPreconnected U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ u ∈ U, f u ≠ 0) :
  ∀ (hu : u ∈ U), (h₁f u hu).order.toNat = (h₁f u hu).order := by

@ -221,7 +221,7 @@ theorem discreteZeros
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hU : IsPreconnected U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ u ∈ U, f u ≠ 0) :
  DiscreteTopology ((U.restrict f)⁻¹' {0}) := by

@ -293,7 +293,7 @@ theorem finiteZeros
  {U : Set ℂ}
  (h₁U : IsPreconnected U)
  (h₂U : IsCompact U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ u ∈ U, f u ≠ 0) :
  Set.Finite (U.restrict f⁻¹' {0}) := by

@ -310,14 +310,14 @@ theorem finiteZeros
  exact discreteZeros h₁U h₁f h₂f


-theorem AnalyticOnNhdCompact.eliminateZeros
+theorem AnalyticOnCompact.eliminateZeros
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁U : IsPreconnected U)
  (h₂U : IsCompact U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by
+  ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by

  let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset

@ -325,13 +325,13 @@ theorem AnalyticOnNhdCompact.eliminateZeros

  have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
    intro a _
-    dsimp [n, AnalyticOnNhd.order]
+    dsimp [n, AnalyticOn.order]
    rw [eq_comm]
    apply XX h₁U
    exact h₂f


-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
  use g
  use A

@ -357,14 +357,14 @@ theorem AnalyticOnNhdCompact.eliminateZeros
    · exact inter


-theorem AnalyticOnNhdCompact.eliminateZeros₂
+theorem AnalyticOnCompact.eliminateZeros₂
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁U : IsPreconnected U)
  (h₂U : IsCompact U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by
+  ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by

  let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset

@ -372,12 +372,12 @@ theorem AnalyticOnNhdCompact.eliminateZeros₂

  have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
    intro a _
-    dsimp [n, AnalyticOnNhd.order]
+    dsimp [n, AnalyticOn.order]
    rw [eq_comm]
    apply XX h₁U
    exact h₂f

-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
  use g

  have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
@ -402,14 +402,14 @@ theorem AnalyticOnNhdCompact.eliminateZeros₂
    · exact h₃g


-theorem AnalyticOnNhdCompact.eliminateZeros₁
+theorem AnalyticOnCompact.eliminateZeros₁
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁U : IsPreconnected U)
  (h₂U : IsCompact U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by
+  ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by

  let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset

@ -417,12 +417,12 @@ theorem AnalyticOnNhdCompact.eliminateZeros₁

  have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
    intro a _
-    dsimp [n, AnalyticOnNhd.order]
+    dsimp [n, AnalyticOn.order]
    rw [eq_comm]
    apply XX h₁U
    exact h₂f

-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
  use g

  have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
--- a/Nevanlinna/bilinear.lean
+++ b/Nevanlinna/bilinear.lean
@ -28,7 +28,7 @@ orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`.

 -/

-open InnerProductSpace
+
 open TensorProduct


@ -41,11 +41,12 @@ noncomputable def InnerProductSpace.canonicalCovariantTensor
  (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  : E ⊗[ℝ] E := ∑ i, ((stdOrthonormalBasis ℝ E) i) ⊗ₜ[ℝ] ((stdOrthonormalBasis ℝ E) i)

+
 theorem InnerProductSpace.canonicalCovariantTensorRepresentation
  (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [Fintype ι]
-  (v : OrthonormalBasis ι ℝ E) :
-  InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by
+  (v : OrthonormalBasis ι ℝ E)
+  : InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by

  let w := stdOrthonormalBasis ℝ E
  conv =>
--- a/Nevanlinna/cauchyRiemann.lean
+++ b/Nevanlinna/cauchyRiemann.lean
@ -31,7 +31,7 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
  have ContinuousLinearMap.comp_lineDeriv : ∀ w : ℂ, ∀ l : ℂ →L[ℝ] ℝ, lineDeriv ℝ (l ∘ f) z w = l ((fderiv ℝ f z) w) := by
    intro w l
    rw [DifferentiableAt.lineDeriv_eq_fderiv]
-    rw [fderiv_comp]
+    rw [fderiv.comp]
    simp
    fun_prop
    exact h.restrictScalars ℝ
--- a/Nevanlinna/divisor.lean
+++ b/Nevanlinna/divisor.lean
@ -1,93 +0,0 @@
-import Mathlib.Analysis.SpecialFunctions.Integrals
-import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
-import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
-import Nevanlinna.analyticAt
-import Nevanlinna.mathlibAddOn
-
-open Interval Topology
-open Real Filter MeasureTheory intervalIntegral
-
-
-structure Divisor
-  (U : Set ℂ)
-  where
-  toFun : ℂ → ℤ
-  supportInU : toFun.support ⊆ U
-  locallyFiniteInU : ∀ x ∈ U, toFun =ᶠ[𝓝[≠] x] 0
-
-instance
-  (U : Set ℂ) :
-  CoeFun (Divisor U) (fun _ ↦ ℂ → ℤ) where
-  coe := Divisor.toFun
-
-attribute [coe] Divisor.toFun
-
-
-theorem Divisor.discreteSupport
-  {U : Set ℂ}
-  (hU : IsClosed U)
-  (D : Divisor U) :
-  DiscreteTopology D.toFun.support := by
-  apply discreteTopology_subtype_iff.mpr
-  intro x hx
-  apply inf_principal_eq_bot.mpr
-  by_cases h₁x : x ∈ U
-  · let A := D.locallyFiniteInU x h₁x
-    refine mem_nhdsWithin.mpr ?_
-    rw [eventuallyEq_nhdsWithin_iff] at A
-    obtain ⟨U, h₁U, h₂U, h₃U⟩ := eventually_nhds_iff.1 A
-    use U
-    constructor
-    · exact h₂U
-    · constructor
-      · exact h₃U
-      · intro y hy
-        let C := h₁U y hy.1 hy.2
-        tauto
-  · refine mem_nhdsWithin.mpr ?_
-    use Uᶜ
-    constructor
-    · simpa
-    · constructor
-      · tauto
-      · intro y _
-        let A := D.supportInU
-        simp at A
-        simp
-        exact False.elim (h₁x (A x hx))
-
-
-
-theorem Divisor.closedSupport
-  {U : Set ℂ}
-  (hU : IsClosed U)
-  (D : Divisor U) :
-  IsClosed D.toFun.support := by
-
-  rw [← isOpen_compl_iff]
-  rw [isOpen_iff_eventually]
-  intro x hx
-  by_cases h₁x : x ∈ U
-  · have A := D.locallyFiniteInU x h₁x
-    simp [A]
-    simp at hx
-    let B := Mnhds A hx
-    simpa
-  · rw [eventually_iff_exists_mem]
-    use Uᶜ
-    constructor
-    · exact IsClosed.compl_mem_nhds hU h₁x
-    · intro y hy
-      simp
-      exact Function.nmem_support.mp fun a => hy (D.supportInU a)
-
-
-theorem Divisor.finiteSupport
-  {U : Set ℂ}
-  (hU : IsCompact U)
-  (D : Divisor U) :
-  Set.Finite D.toFun.support := by
-  apply IsCompact.finite
-  · apply IsCompact.of_isClosed_subset hU (D.closedSupport hU.isClosed)
-    exact D.supportInU
-  · exact D.discreteSupport hU.isClosed
--- a/Nevanlinna/firstMain.lean
+++ b/Nevanlinna/firstMain.lean
@ -1,19 +1,15 @@
-import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.holomorphic_JensenFormula

 open Real

-variable (f : ℂ → ℂ)
-variable {h₁f : MeromorphicOn f ⊤}
+variable {f : ℂ → ℂ}
+variable {h₁f : AnalyticOn ℂ f ⊤}
 variable {h₂f : f 0 ≠ 0}

-
-
-noncomputable def Nevanlinna.n : ℝ → ℤ := by
+noncomputable def unintegratedCounting : ℝ → ℕ := by
  intro r
-  have : MeromorphicAt f z := by
-    exact h₁f (sorryAx ℂ true) trivial
-  exact ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (h₁f z trivial).order
+  let A := h₁f.mono (by tauto : Metric.closedBall (0 : ℂ) r ⊆ ⊤)
+  exact ∑ᶠ z, (A.order z).toNat

 noncomputable def integratedCounting : ℝ → ℝ := by
  intro r
--- a/Nevanlinna/holomorphic_JensenFormula.lean
+++ b/Nevanlinna/holomorphic_JensenFormula.lean
@ -1,6 +1,6 @@
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Analysis.Analytic.IsolatedZeros
-import Nevanlinna.analyticOnNhd_zeroSet
+import Nevanlinna.analyticOn_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 import Nevanlinna.specialFunctions_CircleIntegral_affine
@ -11,7 +11,7 @@ open Real

 theorem jensen_case_R_eq_one
  (f : ℂ → ℂ)
-  (h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 1))
+  (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 1))
  (h₂f : f 0 ≠ 0) :
  log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by

@ -24,7 +24,7 @@ theorem jensen_case_R_eq_one
  have h'₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
    use 0; simp; exact h₂f

-  obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnNhdCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f
+  obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f

  have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by
    intro z h₁z
@ -259,9 +259,9 @@ theorem jensen_case_R_eq_one
  intro x ⟨h₁x, _⟩
  simp

-  dsimp [AnalyticOnNhd.order] at h₁x
+  dsimp [AnalyticOn.order] at h₁x
  simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x
-  exact AnalyticAt.supp_order_toNat (AnalyticOnNhd.order.proof_1 h₁f x) h₁x
+  exact AnalyticAt.supp_order_toNat (AnalyticOn.order.proof_1 h₁f x) h₁x

  --
  intro x hx
@ -297,7 +297,7 @@ theorem jensen
  {R : ℝ}
  (hR : 0 < R)
  (f : ℂ → ℂ)
-  (h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 R))
+  (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 R))
  (h₂f : f 0 ≠ 0) :
  log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by

@ -327,8 +327,8 @@ theorem jensen

  let F := f ∘ ℓ

-  have h₁F : AnalyticOnNhd ℂ F (Metric.closedBall 0 1) := by
-    apply AnalyticOnNhd.comp (t := Metric.closedBall 0 R)
+  have h₁F : AnalyticOn ℂ F (Metric.closedBall 0 1) := by
+    apply AnalyticOn.comp (t := Metric.closedBall 0 R)
    exact h₁f
    intro x _
    apply ℓ.toContinuousLinearMap.analyticAt x
@ -430,7 +430,7 @@ theorem jensen
  left
  congr 1

-  dsimp [AnalyticOnNhd.order]
+  dsimp [AnalyticOn.order]
  rw [← AnalyticAt.order_comp_CLE ℓ]

  --
--- a/Nevanlinna/holomorphic_examples.lean
+++ b/Nevanlinna/holomorphic_examples.lean
@ -277,7 +277,7 @@ theorem harmonic_is_realOfHolomorphic

    intro x hx
    rw [fderivWithin_eq_fderiv, fderivWithin_eq_fderiv]
-    rw [fderiv_comp]
+    rw [fderiv.comp]
    simp
    apply ContinuousLinearMap.ext
    intro w
--- a/Nevanlinna/holomorphic_primitive.lean
+++ b/Nevanlinna/holomorphic_primitive.lean
@ -666,7 +666,7 @@ theorem primitive_additivity'
      dsimp [ε']; simp
      have : |ε| = ε := by apply abs_of_pos h₁ε
      rw [this]
-      apply (inv_mul_lt_iff₀ zero_lt_two).mpr
+      apply (inv_mul_lt_iff zero_lt_two).mpr
      linarith
    have h₁ε' : 0 < ε' := by
      apply mul_pos _ h₁ε
--- a/Nevanlinna/holomorphic_zero.lean
+++ b/Nevanlinna/holomorphic_zero.lean
@ -3,7 +3,7 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Mathlib.Topology.ContinuousOn
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Nevanlinna.holomorphic
-import Nevanlinna.analyticOnNhd_zeroSet
+import Nevanlinna.analyticOn_zeroSet


 noncomputable def zeroDivisor
@ -134,7 +134,7 @@ theorem topOnPreconnected
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hU : IsPreconnected U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) :
  ∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by

@ -143,7 +143,7 @@ theorem topOnPreconnected
  obtain ⟨z', hz'⟩ := H
  rw [AnalyticAt.order_eq_top_iff] at hz'
  rw [← AnalyticAt.frequently_zero_iff_eventually_zero (h₁f z z')] at hz'
-  have A := AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
+  have A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
  tauto


@ -151,7 +151,7 @@ theorem supportZeroSet
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hU : IsPreconnected U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) :
  U ∩ Function.support (zeroDivisor f) = U ∩ f⁻¹' {0} := by

@ -180,7 +180,7 @@ theorem supportZeroSet
          refine Eq.symm (ENat.coe_toNat ?h.mpr.right.right.right.a)
          exact topOnPreconnected hU h₁f h₂f h₁x

-/-
+
 theorem discreteZeros
  {f : ℂ → ℂ} :
  DiscreteTopology (Function.support (zeroDivisor f)) := by
@ -254,13 +254,13 @@ theorem discreteZeros
  simp [this] at F
  ext
  rwa [sub_eq_zero] at F
-/
+

 theorem zeroDivisor_finiteOnCompact
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (hU : IsPreconnected U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) -- not needed!
  (h₂U : IsCompact U) :
  Set.Finite (U ∩ Function.support (zeroDivisor f)) := by
@ -289,7 +289,7 @@ noncomputable def zeroDivisorDegree
  {U : Set ℂ}
  (h₁U : IsPreconnected U) -- not needed!
  (h₂U : IsCompact U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
  ℕ := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset.card

@ -299,7 +299,7 @@ lemma zeroDivisorDegreeZero
  {U : Set ℂ}
  (h₁U : IsPreconnected U) -- not needed!
  (h₂U : IsCompact U)
-  (h₁f : AnalyticOnNhd ℂ f U)
+  (h₁f : AnalyticOn ℂ f U)
  (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
  0 = zeroDivisorDegree h₁U h₂U h₁f h₂f ↔ U ∩ (zeroDivisor f).support = ∅ := by
  sorry
@ -309,9 +309,9 @@ lemma eliminatingZeros₀
  {U : Set ℂ}
  (h₁U : IsPreconnected U)
  (h₂U : IsCompact U) :
-  ∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOnNhd ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
+  ∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOn ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
  (n = zeroDivisorDegree h₁U h₂U h₁f h₂f) →
-  ∃ F : ℂ → ℂ, (AnalyticOnNhd ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by
+  ∃ F : ℂ → ℂ, (AnalyticOn ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by

  intro n
  induction' n with n ih
@ -340,7 +340,7 @@ lemma eliminatingZeros₀



-  let A := AnalyticOnNhd.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀)
+  let A := AnalyticOn.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀)
  let B := zeroDivisor_eq_ord_AtZeroDivisorSupport hz₀.2
  let B := zeroDivisor_eq_ord_AtZeroDivisorSupport' hz₀.2
  rw [eq_comm] at B
--- a/Nevanlinna/junk/laplace2.lean
+++ b/Nevanlinna/junk/laplace2.lean
--- a/Nevanlinna/mathlibAddOn.lean
+++ b/Nevanlinna/mathlibAddOn.lean
@ -1,7 +1,5 @@
-import Mathlib.Analysis.Analytic.Meromorphic
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Add
-import Nevanlinna.analyticAt

 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
@ -35,42 +33,3 @@ theorem ContDiff.const_smul' {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
  have : c • f = fun x ↦ c • f x := rfl
  rw [this]
  exact ContDiff.const_smul c hf
-
-
-
-open Topology Filter
-
-lemma Mnhds
-  {α : Type}
-  {f g : ℂ → α}
-  {z₀ : ℂ}
-  (h₁ : f =ᶠ[𝓝[≠] z₀] g)
-  (h₂ : f z₀ = g z₀) :
-  f =ᶠ[𝓝 z₀] g := by
-  apply eventually_nhds_iff.2
-  obtain ⟨t, h₁t, h₂t⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₁)
-  use t
-  constructor
-  · intro y hy
-    by_cases h₂y : y ∈ ({z₀}ᶜ : Set ℂ)
-    · exact h₁t y hy h₂y
-    · simp at h₂y
-      rwa [h₂y]
-  · exact h₂t
-
-- unclear where this should go
-
-lemma WithTopCoe
-  {n : WithTop ℕ} :
-  WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by
-  rcases n with h|h
-  · intro h
-    contradiction
-  · intro h₁
-    simp only [WithTop.map, Option.map] at h₁
-    have : (h : ℤ) = 0 := by
-      exact WithTop.coe_eq_zero.mp h₁
-    have : h = 0 := by
-      exact Int.ofNat_eq_zero.mp this
-    rw [this]
-    rfl
--- a/Nevanlinna/meromorphicAt.lean
+++ b/Nevanlinna/meromorphicAt.lean
@ -1,147 +0,0 @@
-import Mathlib.Analysis.Analytic.Meromorphic
-import Nevanlinna.analyticAt
-import Nevanlinna.divisor
-
-
-open scoped Interval Topology
-open Real Filter MeasureTheory intervalIntegral
-
-
-theorem meromorphicAt_congr
-  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
-  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
-  (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
-  ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩
-
-
-theorem meromorphicAt_congr'
-  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
-  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
-  (h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
-  meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds)
-
-
-theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
-  (∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) ∨ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0 := by
-
-  obtain ⟨n, h⟩ := hf
-  let A := h.eventually_eq_zero_or_eventually_ne_zero
-
-  rw [eventually_nhdsWithin_iff]
-  rw [eventually_nhds_iff]
-  rcases A with h₁|h₂
-  · rw [eventually_nhds_iff] at h₁
-    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₁
-    left
-    use N
-    constructor
-    · intro y h₁y h₂y
-      let A := h₁N y h₁y
-      simp at A
-      rcases A with h₃|h₄
-      · let B := h₃.1
-        simp at h₂y
-        let C := sub_eq_zero.1 B
-        tauto
-      · assumption
-    · constructor
-      · exact h₂N
-      · exact h₃N
-  · right
-    rw [eventually_nhdsWithin_iff]
-    rw [eventually_nhds_iff]
-    rw [eventually_nhdsWithin_iff] at h₂
-    rw [eventually_nhds_iff] at h₂
-    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₂
-    use N
-    constructor
-    · intro y h₁y h₂y
-      by_contra h
-      let A := h₁N y h₁y h₂y
-      rw [h] at A
-      simp at A
-    · constructor
-      · exact h₂N
-      · exact h₃N
-
-
-theorem MeromorphicAt.order_congr
-  {f₁ f₂ : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf₁ : MeromorphicAt f₁ z₀)
-  (h : f₁ =ᶠ[𝓝[≠] z₀] f₂):
-  hf₁.order = (hf₁.congr h).order := by
-  by_cases hord : hf₁.order = ⊤
-  · rw [hord, eq_comm]
-    rw [hf₁.order_eq_top_iff] at hord
-    rw [(hf₁.congr h).order_eq_top_iff]
-    exact EventuallyEq.rw hord (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))
-  · obtain ⟨n, hn : hf₁.order = n⟩ := Option.ne_none_iff_exists'.mp hord
-    obtain ⟨g, h₁g, h₂g, h₃g⟩ := (hf₁.order_eq_int_iff n).1 hn
-    rw [hn, eq_comm, (hf₁.congr h).order_eq_int_iff]
-    use g
-    constructor
-    · assumption
-    · constructor
-      · assumption
-      · exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))
-
-
-theorem MeromorphicAt.order_mul
-  {f₁ f₂ : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf₁ : MeromorphicAt f₁ z₀)
-  (hf₂ : MeromorphicAt f₂ z₀) :
-  (hf₁.mul hf₂).order = hf₁.order + hf₂.order := by
-  by_cases h₂f₁ : hf₁.order = ⊤
-  · simp [h₂f₁]
-    rw [hf₁.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₁
-    rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
-    obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
-    use t
-    constructor
-    · intro y h₁y h₂y
-      simp; left
-      rw [h₁t y h₁y h₂y]
-    · exact ⟨h₂t, h₃t⟩
-  · by_cases h₂f₂ : hf₂.order = ⊤
-    · simp [h₂f₂]
-      rw [hf₂.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₂
-      rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
-      obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
-      use t
-      constructor
-      · intro y h₁y h₂y
-        simp; right
-        rw [h₁t y h₁y h₂y]
-      · exact ⟨h₂t, h₃t⟩
-    · have h₃f₁ := Eq.symm (WithTop.coe_untop hf₁.order h₂f₁)
-      have h₃f₂ := Eq.symm (WithTop.coe_untop hf₂.order h₂f₂)
-      obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (hf₁.order_eq_int_iff (hf₁.order.untop h₂f₁)).1 h₃f₁
-      obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (hf₂.order_eq_int_iff (hf₂.order.untop h₂f₂)).1 h₃f₂
-      rw [h₃f₁, h₃f₂, ← WithTop.coe_add]
-      rw [MeromorphicAt.order_eq_int_iff]
-      use g₁ * g₂
-      constructor
-      · exact AnalyticAt.mul h₁g₁ h₁g₂
-      · constructor
-        · simp; tauto
-        · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₁)
-          obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₂)
-          rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
-          use t₁ ∩ t₂
-          constructor
-          · intro y h₁y h₂y
-            simp
-            rw [h₁t₁ y h₁y.1 h₂y, h₁t₂ y h₁y.2 h₂y]
-            simp
-            rw [zpow_add' (by left; exact sub_ne_zero_of_ne h₂y)]
-            group
-          · constructor
-            · exact IsOpen.inter h₂t₁ h₂t₂
-            · exact Set.mem_inter h₃t₁ h₃t₂
--- a/Nevanlinna/meromorphicOn.lean
+++ b/Nevanlinna/meromorphicOn.lean
@ -1,55 +0,0 @@
-import Mathlib.Analysis.Analytic.Meromorphic
-import Nevanlinna.analyticAt
-import Nevanlinna.divisor
-import Nevanlinna.meromorphicAt
-import Nevanlinna.meromorphicOn_divisor
-import Nevanlinna.stronglyMeromorphicOn
-import Nevanlinna.mathlibAddOn
-
-open scoped Interval Topology
-open Real Filter MeasureTheory intervalIntegral
-
-theorem MeromorphicOn.open_of_order_eq_top
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁f : MeromorphicOn f U) :
-  IsOpen { u : U | (h₁f u.1 u.2).order = ⊤ } := by
-
-  apply isOpen_iff_forall_mem_open.mpr
-  intro z hz
-  simp at hz
-  rw [MeromorphicAt.order_eq_top_iff] at hz
-  rw [eventually_nhdsWithin_iff] at hz
-  rw [eventually_nhds_iff] at hz
-  obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
-  let t :=
-  have : t ⊆ { u : U | (h₁f u.1 u.2).order = ⊤} := by
-    sorry
-
-
-
-  rw [← eventually_eventually_nhds] at hz
-
-
-  sorry
-
-
-theorem MeromorphicOn.order_ne_top
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsConnected U)
-  (h₁f : MeromorphicOn f U) :
-  (∃ z₀ : U, (h₁f z₀.1 z₀.2).order = ⊤) ↔ (∀ z : U, (h₁f z.1 z.2).order = ⊤) := by
-
-  constructor
-  · intro h
-    obtain ⟨h₁z₀, h₂z₀⟩ := h
-    intro hz
-
-
-    sorry
-
-  · intro h
-    obtain ⟨w, hw⟩ := h₁U.nonempty
-    use ⟨w, hw⟩
-    exact h ⟨w, hw⟩
--- a/Nevanlinna/meromorphicOn_divisor.lean
+++ b/Nevanlinna/meromorphicOn_divisor.lean
@ -1,76 +0,0 @@
-import Mathlib.Analysis.Analytic.Meromorphic
-import Nevanlinna.analyticAt
-import Nevanlinna.divisor
-import Nevanlinna.meromorphicAt
-
-
-open scoped Interval Topology
-open Real Filter MeasureTheory intervalIntegral
-
-
-noncomputable def MeromorphicOn.divisor
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : MeromorphicOn f U) :
-  Divisor U where
-
-  toFun := by
-    intro z
-    if hz : z ∈ U then
-      exact ((hf z hz).order.untop' 0 : ℤ)
-    else
-      exact 0
-
-  supportInU := by
-    intro z hz
-    simp at hz
-    by_contra h₂z
-    simp [h₂z] at hz
-
-  locallyFiniteInU := by
-    intro z hz
-
-    apply eventually_nhdsWithin_iff.2
-    rw [eventually_nhds_iff]
-
-    rcases MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h
-    · rw [eventually_nhdsWithin_iff] at h
-      rw [eventually_nhds_iff] at h
-      obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
-      use N
-      constructor
-      · intro y h₁y h₂y
-        by_cases h₃y : y ∈ U
-        · simp [h₃y]
-          right
-          rw [MeromorphicAt.order_eq_top_iff (hf y h₃y)]
-          rw [eventually_nhdsWithin_iff]
-          rw [eventually_nhds_iff]
-          use N ∩ {z}ᶜ
-          constructor
-          · intro x h₁x _
-            exact h₁N x h₁x.1 h₁x.2
-          · constructor
-            · exact IsOpen.inter h₂N isOpen_compl_singleton
-            · exact Set.mem_inter h₁y h₂y
-        · simp [h₃y]
-      · tauto
-
-    · let A := (hf z hz).eventually_analyticAt
-      let B := Filter.eventually_and.2 ⟨h, A⟩
-      rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at B
-      obtain ⟨N, h₁N, h₂N, h₃N⟩ := B
-      use N
-      constructor
-      · intro y h₁y h₂y
-        by_cases h₃y : y ∈ U
-        · simp [h₃y]
-          left
-          rw [(h₁N y h₁y h₂y).2.meromorphicAt_order]
-          let D := (h₁N y h₁y h₂y).2.order_eq_zero_iff.2
-          let C := (h₁N y h₁y h₂y).1
-          let E := D C
-          rw [E]
-          simp
-        · simp [h₃y]
-      · tauto
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@ -202,14 +202,14 @@ theorem partialDeriv_compContLin
    left
    intro w
    left
-    rw [fderiv_comp w (ContinuousLinearMap.differentiableAt l) (h w)]
+    rw [fderiv.comp w (ContinuousLinearMap.differentiableAt l) (h w)]
  simp
  rfl


 theorem partialDeriv_compContLinAt {f : E → F} {l : F →L[𝕜] G} {v : E} {x : E} (h : DifferentiableAt 𝕜 f x) : (partialDeriv 𝕜 v (l ∘ f)) x = (l ∘ partialDeriv 𝕜 v f) x:= by
  unfold partialDeriv
-  rw [fderiv_comp x (ContinuousLinearMap.differentiableAt l) h]
+  rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
  simp


--- a/Nevanlinna/specialFunctions_Integral_log_sin.lean
+++ b/Nevanlinna/specialFunctions_Integral_log_sin.lean
@ -24,7 +24,7 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((
    exact zero_lt_two
    apply (Set.mem_Icc.1 hx).1
    simp
-    apply mul_le_one₀
+    apply mul_le_one
    rw [div_le_one pi_pos]
    exact two_le_pi
    exact (Set.mem_Icc.1 hx).1
--- a/Nevanlinna/stronglyMeromorphicAt.lean
+++ b/Nevanlinna/stronglyMeromorphicAt.lean
@ -1,437 +0,0 @@
-import Mathlib.Analysis.Analytic.Meromorphic
-import Mathlib.Algebra.Order.AddGroupWithTop
-import Nevanlinna.analyticAt
-import Nevanlinna.mathlibAddOn
-import Nevanlinna.meromorphicAt
-
-
-open Topology
-
-
-/- Strongly MeromorphicAt -/
-def StronglyMeromorphicAt
-  (f : ℂ → ℂ)
-  (z₀ : ℂ) :=
-  (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℤ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))
-
-
-
-/- Strongly MeromorphicAt is Meromorphic -/
-theorem StronglyMeromorphicAt.meromorphicAt
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : StronglyMeromorphicAt f z₀) :
-  MeromorphicAt f z₀ := by
-  rcases hf with h|h
-  · use 0; simp
-    rw [analyticAt_congr h]
-    exact analyticAt_const
-  · obtain ⟨n, g, h₁g, _, h₃g⟩ := h
-    rw [meromorphicAt_congr' h₃g]
-    apply MeromorphicAt.smul
-    apply MeromorphicAt.zpow
-    apply MeromorphicAt.sub
-    apply MeromorphicAt.id
-    apply MeromorphicAt.const
-    exact AnalyticAt.meromorphicAt h₁g
-
-
-/- Strongly MeromorphicAt of non-negative order is analytic -/
-theorem StronglyMeromorphicAt.analytic
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (h₁f : StronglyMeromorphicAt f z₀)
-  (h₂f : 0 ≤ h₁f.meromorphicAt.order):
-  AnalyticAt ℂ f z₀ := by
-  let h₁f' := h₁f
-  rcases h₁f' with h|h
-  · rw [analyticAt_congr h]
-    exact analyticAt_const
-  · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h
-    rw [analyticAt_congr h₃g]
-
-    have : h₁f.meromorphicAt.order = n := by
-      rw [MeromorphicAt.order_eq_int_iff]
-      use g
-      constructor
-      · exact h₁g
-      · constructor
-        · exact h₂g
-        · exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds
-    rw [this] at h₂f
-    apply AnalyticAt.smul
-    nth_rw 1 [← Int.toNat_of_nonneg (WithTop.coe_nonneg.mp h₂f)]
-    apply AnalyticAt.pow
-    apply AnalyticAt.sub
-    apply analyticAt_id -- Warning: want apply AnalyticAt.id
-    apply analyticAt_const -- Warning: want AnalyticAt.const
-    exact h₁g
-
-
-/- Analytic functions are strongly meromorphic -/
-theorem AnalyticAt.stronglyMeromorphicAt
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (h₁f : AnalyticAt ℂ f z₀) :
-  StronglyMeromorphicAt f z₀ := by
-  by_cases h₂f : h₁f.order = ⊤
-  · rw [AnalyticAt.order_eq_top_iff] at h₂f
-    tauto
-  · have : h₁f.order ≠ ⊤ := h₂f
-    rw [← ENat.coe_toNat_eq_self] at this
-    rw [eq_comm, AnalyticAt.order_eq_nat_iff] at this
-    right
-    use h₁f.order.toNat
-    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
-    use g
-    tauto
-
-
-/- Strong meromorphic depends only on germ -/
-theorem stronglyMeromorphicAt_congr
-  {f g : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hfg : f =ᶠ[𝓝 z₀] g) :
-  StronglyMeromorphicAt f z₀ ↔ StronglyMeromorphicAt g z₀ := by
-  unfold StronglyMeromorphicAt
-  constructor
-  · intro h
-    rcases h with h|h
-    · left
-      exact Filter.EventuallyEq.rw h (fun x => Eq (g x)) (id (Filter.EventuallyEq.symm hfg))
-    · obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
-      right
-      use n
-      use h
-      constructor
-      · assumption
-      · constructor
-        · assumption
-        · apply Filter.EventuallyEq.trans hfg.symm
-          assumption
-  · intro h
-    rcases h with h|h
-    · left
-      exact Filter.EventuallyEq.rw h (fun x => Eq (f x)) hfg
-    · obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
-      right
-      use n
-      use h
-      constructor
-      · assumption
-      · constructor
-        · assumption
-        · apply Filter.EventuallyEq.trans hfg
-          assumption
-
-
-theorem StronglyMeromorphicAt.order_eq_zero_iff
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : StronglyMeromorphicAt f z₀) :
-  hf.meromorphicAt.order = 0 ↔ f z₀ ≠ 0 := by
-  constructor
-  · intro h₁f
-    let A := hf.analytic (le_of_eq (id (Eq.symm h₁f)))
-    apply A.order_eq_zero_iff.1
-    let B := A.meromorphicAt_order
-    rw [h₁f] at B
-    apply WithTopCoe
-    rw [eq_comm]
-    exact B
-  · intro h
-    have hf' := hf
-    rcases hf with h₁|h₁
-    · have : f z₀ = 0 := by
-        apply Filter.EventuallyEq.eq_of_nhds h₁
-      tauto
-    · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁
-      have : n = 0 := by
-        by_contra hContra
-        let A := Filter.EventuallyEq.eq_of_nhds h₃g
-        have : (0 : ℂ) ^ n = 0 := by
-          exact zero_zpow n hContra
-        simp at A
-        simp_rw [this] at A
-        simp at A
-        tauto
-      rw [this] at h₃g
-      simp at h₃g
-
-      have : hf'.meromorphicAt.order = 0 := by
-        apply (hf'.meromorphicAt.order_eq_int_iff 0).2
-        use g
-        constructor
-        · assumption
-        · constructor
-          · assumption
-          · simp
-            apply Filter.EventuallyEq.filter_mono h₃g
-            exact nhdsWithin_le_nhds
-      exact this
-
-
-theorem StronglyMeromorphicAt.localIdentity
-  {f g : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : StronglyMeromorphicAt f z₀)
-  (hg : StronglyMeromorphicAt g z₀) :
-  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
-
-  intro h
-
-  have t₀ : hf.meromorphicAt.order = hg.meromorphicAt.order := by
-    exact hf.meromorphicAt.order_congr h
-
-  by_cases cs : hf.meromorphicAt.order = 0
-  · rw [cs] at t₀
-    have h₁f := hf.analytic (le_of_eq (id (Eq.symm cs)))
-    have h₁g := hg.analytic (le_of_eq t₀)
-    exact h₁f.localIdentity h₁g h
-  · apply Mnhds h
-    let A := cs
-    rw [hf.order_eq_zero_iff] at A
-    simp at A
-    let B := cs
-    rw [t₀] at B
-    rw [hg.order_eq_zero_iff] at B
-    simp at B
-    rw [A, B]
-
-
-
-/- Make strongly MeromorphicAt -/
-noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
-  ℂ → ℂ := by
-  intro z
-  by_cases z = z₀
-  · by_cases h₁f : hf.order = (0 : ℤ)
-    · rw [hf.order_eq_int_iff] at h₁f
-      exact (Classical.choose h₁f) z₀
-    · exact 0
-  · exact f z
-
-
-lemma m₁
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
-  ∀ z ≠ z₀, f z = hf.makeStronglyMeromorphicAt z := by
-  intro z hz
-  unfold MeromorphicAt.makeStronglyMeromorphicAt
-  simp [hz]
-
-
-lemma m₂
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
-  f =ᶠ[𝓝[≠] z₀] hf.makeStronglyMeromorphicAt := by
-  apply eventually_nhdsWithin_of_forall
-  exact fun x a => m₁ hf x a
-
-
-theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicAt f z₀) :
-  StronglyMeromorphicAt hf.makeStronglyMeromorphicAt z₀ := by
-
-  by_cases h₂f : hf.order = ⊤
-  · have : hf.makeStronglyMeromorphicAt =ᶠ[𝓝 z₀] 0 := by
-      apply Mnhds
-      · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
-        exact (MeromorphicAt.order_eq_top_iff hf).1 h₂f
-      · unfold MeromorphicAt.makeStronglyMeromorphicAt
-        simp [h₂f]
-
-    apply AnalyticAt.stronglyMeromorphicAt
-    rw [analyticAt_congr this]
-    apply analyticAt_const
-  · let n := hf.order.untop h₂f
-    have : hf.order = n := by
-      exact Eq.symm (WithTop.coe_untop hf.order h₂f)
-    rw [hf.order_eq_int_iff] at this
-    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
-    right
-    use n
-    use g
-    constructor
-    · assumption
-    · constructor
-      · assumption
-      · apply Mnhds
-        · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
-          exact h₃g
-        · unfold MeromorphicAt.makeStronglyMeromorphicAt
-          simp
-          by_cases h₃f : hf.order = (0 : ℤ)
-          · let h₄f := (hf.order_eq_int_iff 0).1 h₃f
-            simp [h₃f]
-            obtain ⟨h₁G, h₂G, h₃G⟩  := Classical.choose_spec h₄f
-            simp at h₃G
-            have hn : n = 0 := Eq.symm ((fun {α} {a} {b} h => (WithTop.eq_untop_iff h).mpr) h₂f (id (Eq.symm h₃f)))
-            rw [hn]
-            rw [hn] at h₃g; simp at h₃g
-            simp
-            have : g =ᶠ[𝓝 z₀] (Classical.choose h₄f) := by
-              apply h₁g.localIdentity h₁G
-              exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G
-            rw [Filter.EventuallyEq.eq_of_nhds this]
-          · have : hf.order ≠ 0 := h₃f
-            simp [this]
-            left
-            apply zero_zpow n
-            dsimp [n]
-            rwa [WithTop.untop_eq_iff h₂f]
-
-
-theorem makeStronglyMeromorphic_id
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : StronglyMeromorphicAt f z₀) :
-  f = hf.meromorphicAt.makeStronglyMeromorphicAt := by
-
-  funext z
-  by_cases hz : z = z₀
-  · rw [hz]
-    unfold MeromorphicAt.makeStronglyMeromorphicAt
-    simp
-    have h₀f := hf
-    rcases hf with h₁f|h₁f
-    · have A : f =ᶠ[𝓝[≠] z₀] 0 := by
-        apply Filter.EventuallyEq.filter_mono h₁f
-        exact nhdsWithin_le_nhds
-      let B := (MeromorphicAt.order_eq_top_iff h₀f.meromorphicAt).2 A
-      simp [B]
-      exact Filter.EventuallyEq.eq_of_nhds h₁f
-    · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁f
-      rw [Filter.EventuallyEq.eq_of_nhds h₃g]
-      have : h₀f.meromorphicAt.order = n := by
-        rw [MeromorphicAt.order_eq_int_iff (StronglyMeromorphicAt.meromorphicAt h₀f) n]
-        use g
-        constructor
-        · assumption
-        · constructor
-          · assumption
-          · exact eventually_nhdsWithin_of_eventually_nhds h₃g
-      by_cases h₃f : h₀f.meromorphicAt.order = 0
-      · simp [h₃f]
-        have hn : n = (0 : ℤ) := by
-          rw [h₃f] at this
-          exact WithTop.coe_eq_zero.mp (id (Eq.symm this))
-        simp_rw [hn]
-        simp
-        let t₀ : h₀f.meromorphicAt.order = (0 : ℤ) := by
-          exact h₃f
-        let A := (h₀f.meromorphicAt.order_eq_int_iff 0).1 t₀
-        have : g =ᶠ[𝓝 z₀] (Classical.choose A) := by
-          obtain ⟨h₀, h₁, h₂⟩  := Classical.choose_spec A
-          apply h₁g.localIdentity h₀
-          rw [hn] at h₃g
-          simp at h₃g
-          simp at h₂
-          have h₄g : f =ᶠ[𝓝[≠] z₀] g := by
-            apply Filter.EventuallyEq.filter_mono h₃g
-            exact nhdsWithin_le_nhds
-          exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₄g) h₂
-        exact Filter.EventuallyEq.eq_of_nhds this
-      · simp [h₃f]
-        left
-        apply zero_zpow n
-        by_contra hn
-        rw [hn] at this
-        tauto
-  · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz
-
-
-theorem StronglyMeromorphicAt.eliminate
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (h₁f : StronglyMeromorphicAt f z₀)
-  (h₂f : h₁f.meromorphicAt.order ≠ ⊤) :
-  ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀)
-    ∧ (g z₀ ≠ 0)
-    ∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by
-
-  let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f
-  let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)
-  have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by
-    apply MeromorphicAt.zpow
-    apply AnalyticAt.meromorphicAt
-    apply AnalyticAt.sub
-    apply analyticAt_id
-    exact analyticAt_const
-  have h₂g₁₁ : h₁g₁₁.order = - h₁f.meromorphicAt.order.untop h₂f := by
-    rw [← WithTop.LinearOrderedAddCommGroup.coe_neg]
-    rw [h₁g₁₁.order_eq_int_iff]
-    use 1
-    constructor
-    · exact analyticAt_const
-    · constructor
-      · simp
-      · apply eventually_nhdsWithin_of_forall
-        simp [g₁₁]
-  have h₁g₁ : MeromorphicAt g₁ z₀ := h₁g₁₁.mul h₁f.meromorphicAt
-  have h₂g₁ : h₁g₁.order = 0 := by
-    rw [h₁g₁₁.order_mul h₁f.meromorphicAt]
-    rw [h₂g₁₁]
-    simp
-    rw [add_comm]
-    rw [LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top h₂f]
-  let g := h₁g₁.makeStronglyMeromorphicAt
-  use g
-  have h₁g : StronglyMeromorphicAt g z₀ := by
-    exact StronglyMeromorphicAt_of_makeStronglyMeromorphic h₁g₁
-  have h₂g : h₁g.meromorphicAt.order = 0 := by
-    rw [← h₁g₁.order_congr (m₂ h₁g₁)]
-    exact h₂g₁
-  constructor
-  · apply analytic
-    · rw [h₂g]
-    · exact h₁g
-  · constructor
-    · rwa [← h₁g.order_eq_zero_iff]
-    · funext z
-      by_cases hz : z = z₀
-      · by_cases hOrd : h₁f.meromorphicAt.order.untop h₂f = 0
-        · simp [hOrd]
-          have : StronglyMeromorphicAt g₁ z₀ := by
-            unfold g₁
-            simp [hOrd]
-            have : (fun z => 1) * f = f := by
-              funext z
-              simp
-            rwa [this]
-          rw [hz]
-          unfold g
-          let A := makeStronglyMeromorphic_id this
-          rw [← A]
-          unfold g₁
-          rw [hOrd]
-          simp
-        · have : h₁f.meromorphicAt.order ≠ 0 := by
-            by_contra hC
-            simp_rw [hC] at hOrd
-            tauto
-          let A := h₁f.order_eq_zero_iff.not.1 this
-          simp at A
-          rw [hz, A]
-          simp
-          left
-          rw [zpow_eq_zero_iff]
-          assumption
-      · simp
-        have : g z = g₁ z := by
-          exact Eq.symm (m₁ h₁g₁ z hz)
-        rw [this]
-        unfold g₁
-        simp [hz]
-        rw [← mul_assoc]
-        rw [mul_inv_cancel₀]
-        simp
-        apply zpow_ne_zero
-        exact sub_ne_zero_of_ne hz
--- a/Nevanlinna/stronglyMeromorphicOn.lean
+++ b/Nevanlinna/stronglyMeromorphicOn.lean
@ -1,112 +0,0 @@
-import Nevanlinna.stronglyMeromorphicAt
-
-
-open Topology
-
-
-/- Strongly MeromorphicOn -/
-def StronglyMeromorphicOn
-  (f : ℂ → ℂ)
-  (U : Set ℂ) :=
-  ∀ z ∈ U, StronglyMeromorphicAt f z
-
-
-/- Strongly MeromorphicAt is Meromorphic -/
-theorem StronglyMeromorphicOn.meromorphicOn
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : StronglyMeromorphicOn f U) :
-  MeromorphicOn f U := by
-  intro z hz
-  exact StronglyMeromorphicAt.meromorphicAt (hf z hz)
-
-
-/- Strongly MeromorphicOn of non-negative order is analytic -/
-theorem StronglyMeromorphicOn.analytic
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁f : StronglyMeromorphicOn f U)
-  (h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ (h₁f x hx).meromorphicAt.order):
-  ∀ z ∈ U, AnalyticAt ℂ f z := by
-  intro z hz
-  apply StronglyMeromorphicAt.analytic
-  exact h₂f z hz
-  exact h₁f z hz
-
-
-/- Analytic functions are strongly meromorphic -/
-theorem AnalyticOn.stronglyMeromorphicOn
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁f : AnalyticOnNhd ℂ f U) :
-  StronglyMeromorphicOn f U := by
-  intro z hz
-  apply AnalyticAt.stronglyMeromorphicAt
-  exact h₁f z hz
-
-
-/- Make strongly MeromorphicAt -/
-noncomputable def MeromorphicOn.makeStronglyMeromorphicOn
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : MeromorphicOn f U) :
-  ℂ → ℂ := by
-  intro z
-  by_cases hz : z ∈ U
-  · exact (hf z hz).makeStronglyMeromorphicAt z
-  · exact f z
-
-
-theorem makeStronglyMeromorphicOn_changeDiscrete
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicOn f U)
-  (hz₀ : z₀ ∈ U) :
-  hf.makeStronglyMeromorphicOn =ᶠ[𝓝[≠] z₀] f := by
-  apply Filter.eventually_iff_exists_mem.2
-  let A := (hf z₀ hz₀).eventually_analyticAt
-  obtain ⟨V, h₁V, h₂V⟩  := Filter.eventually_iff_exists_mem.1 A
-  use V
-  constructor
-  · assumption
-  · intro v hv
-    unfold MeromorphicOn.makeStronglyMeromorphicOn
-    by_cases h₂v : v ∈ U
-    · simp [h₂v]
-      rw [← makeStronglyMeromorphic_id]
-      exact AnalyticAt.stronglyMeromorphicAt (h₂V v hv)
-    · simp [h₂v]
-
-
-theorem StronglyMeromorphicOn_of_makeStronglyMeromorphic
-  {f : ℂ → ℂ}
-  (hf : MeromorphicOn f U) :
-  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
-
-  sorry
-
-
-theorem makeStronglyMeromorphicOn_changeDiscrete'
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicOn f U)
-  (hz₀ : z₀ ∈ U) :
-  hf.makeStronglyMeromorphicOn =ᶠ[𝓝 z₀] (hf z₀ hz₀).makeStronglyMeromorphicAt := by
-  apply Mnhds
-  let A := makeStronglyMeromorphicOn_changeDiscrete hf hz₀
-  apply Filter.EventuallyEq.trans A
-  exact m₂ (hf z₀ hz₀)
-  unfold MeromorphicOn.makeStronglyMeromorphicOn
-  simp [hz₀]
-
-
-theorem StronglyMeromorphicOn_of_makeStronglyMeromorphicOn
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : MeromorphicOn f U) :
-  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
-  intro z₀ hz₀
-  rw [stronglyMeromorphicAt_congr (makeStronglyMeromorphicOn_changeDiscrete' hf hz₀)]
-  exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z₀ hz₀)
--- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
@ -1,86 +0,0 @@
-import Mathlib.Analysis.Analytic.Meromorphic
-import Nevanlinna.analyticAt
-import Nevanlinna.divisor
-import Nevanlinna.meromorphicAt
-import Nevanlinna.meromorphicOn_divisor
-import Nevanlinna.stronglyMeromorphicOn
-import Nevanlinna.mathlibAddOn
-
-
-open scoped Interval Topology
-open Real Filter MeasureTheory intervalIntegral
-
-
-
-theorem MeromorphicOn.decompose
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsConnected U)
-  (h₂U : IsCompact U)
-  (h₁f : MeromorphicOn f U)
-  (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
-  ∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U)
-    ∧ (∀ z ∈ U, g z ≠ 0)
-    ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn ((∏ᶠ p, fun z ↦ (z - p) ^ (h₁f.divisor p)) * g) U) := by
-
-  let g₁ : ℂ → ℂ := f * (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p))
-  have h₁g₁ : MeromorphicOn g₁ U := by
-    sorry
-  let g := h₁g₁.makeStronglyMeromorphicOn
-  have h₁g : MeromorphicOn g U := by
-    sorry
-  have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by
-    sorry
-  have h₃g : StronglyMeromorphicOn g U := by
-    sorry
-  have h₄g : AnalyticOnNhd ℂ g U := by
-    intro z hz
-    apply StronglyMeromorphicAt.analytic (h₃g z hz)
-    rw [h₂g ⟨z, hz⟩]
-  use g
-  constructor
-  · exact h₄g
-  · constructor
-    · intro z hz
-      rw [← (h₄g z hz).order_eq_zero_iff]
-      have A := (h₄g z hz).meromorphicAt_order
-      rw [h₂g ⟨z, hz⟩] at A
-      have t₀ : (h₄g z hz).order ≠ ⊤ := by
-        by_contra hC
-        rw [hC] at A
-        tauto
-      have t₁ : ∃ n : ℕ, (h₄g z hz).order = n := by
-        exact Option.ne_none_iff_exists'.mp t₀
-      obtain ⟨n, hn⟩ := t₁
-      rw [hn] at A
-      apply WithTopCoe
-      rw [eq_comm]
-      rw [hn]
-      exact A
-    · intro z hz
-      have t₀ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ f x := by
-        sorry
-      have t₂ : ∀ᶠ x in 𝓝[≠] z, h₁f.divisor z = 0 := by
-        sorry
-      have t₁ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ (fun z => ∏ᶠ (p : ℂ), (z - p) ^ h₁f.divisor p * g z) x := by
-        sorry
-      apply Filter.EventuallyEq.eq_of_nhds
-      apply StronglyMeromorphicAt.localIdentity
-      · exact StronglyMeromorphicOn_of_makeStronglyMeromorphic h₁f z hz
-      · right
-        use h₁f.divisor z
-        use (∏ᶠ p : ({z}ᶜ : Set ℂ), (fun x ↦ (x - p.1) ^ h₁f.divisor p.1)) * g
-        constructor
-        · apply AnalyticAt.mul₁
-          · apply analyticAt_finprod
-            intro w
-
-
-            sorry
-          · apply (h₃g z hz).analytic
-            rw [h₂g ⟨z, hz⟩]
-        · constructor
-          · sorry
-          · sorry
-
-      sorry
--- a/lake-manifest.json
+++ b/lake-manifest.json
@ -5,17 +5,17 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
+   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
   "name": "batteries",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
-   "configFile": "lakefile.toml"},
+   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/quote4",
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
   "name": "Qq",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
@ -25,7 +25,7 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "de91b59101763419997026c35a41432ac8691f15",
+   "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
   "name": "aesop",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
@ -35,17 +35,17 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
   "name": "proofwidgets",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.46",
+   "inputRev": "v0.0.42",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover/lean4-cli",
   "type": "git",
   "subDir": null,
-   "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
   "name": "Cli",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
@ -55,37 +55,27 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
   "name": "importGraph",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+  {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
   "type": "git",
   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
+   "scope": "",
+   "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
   "name": "LeanSearchClient",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/plausible",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
-   "name": "plausible",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
  {"url": "https://github.com/leanprover-community/mathlib4.git",
   "type": "git",
   "subDir": null,
   "scope": "",
-   "rev": "e3d7d7f053ea862ffb7d1613eff6de0f2e3e8e14",
+   "rev": "4e40837aec257729b3c38dc3e635fc64a7a8a8c1",
   "name": "mathlib",
   "manifestFile": "lake-manifest.json",
   "inputRev": null,
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.12.0-rc1